Theorem: ALL(a):ALL(b):[a ε n & b ε n => P(a) & Q(b)]
         <=> ALL(a):[a ε n => P(a)] & ALL(b):[b ε n => Q(b)

Proof
-----

Normally here, we would have axioms about n. Here, we begin by simply saying n 
is a set. In doing so, we also delay the generalizations about n to the very 
end of the proof.

1	Set(n)
	Premise

	"=>"
	
	Prove: ALL(a):ALL(b):[a ε n & b ε n => P(a) & Q(b)]
	=> ALL(a):[a ε n => P(a)] & ALL(b):[b ε n => Q(b)]
	
	Suppose...

	2	ALL(a):ALL(b):[a ε n & b ε n => P(a) & Q(b)]
		Premise

		Prove: ALL(a):[a ε n => P(a)]
		
		Suppose...

		3	x ε n
			Premise

		Apply premise (line 2) for a=x and b=x

		4	ALL(b):[x ε n & b ε n => P(x) & Q(b)]
			U Spec, 2

		5	x ε n & x ε n => P(x) & Q(x)
			U Spec, 4

		6	x ε n & x ε n
			Join, 3, 3

		Apply detachment

		7	P(x) & Q(x)
			Detach, 5, 6

		8	P(x)
			Split, 7

	As Required:

	9	ALL(a):[a ε n => P(a)]
		Conclusion, 3

		Prove: ALL(b):[b ε n => Q(b)]
		
		Suppose...

		10	x ε n
			Premise

		Again, apply premise (line 2) for a=x and b=x

		11	ALL(b):[x ε n & b ε n => P(x) & Q(b)]
			U Spec, 2

		12	x ε n & x ε n => P(x) & Q(x)
			U Spec, 11

		13	x ε n & x ε n
			Join, 10, 10

		Apply detachment

		14	P(x) & Q(x)
			Detach, 12, 13

		15	Q(x)
			Split, 14

	As Required:

	16	ALL(b):[b ε n => Q(b)]
		Conclusion, 10

	Join results

	17	ALL(a):[a ε n => P(a)] & ALL(b):[b ε n => Q(b)]
		Join, 9, 16

"=>"

As Required:

18	ALL(a):ALL(b):[a ε n & b ε n => P(a) & Q(b)]
	=> ALL(a):[a ε n => P(a)] & ALL(b):[b ε n => Q(b)]
	Conclusion, 2

	"<="
	
	Prove: ALL(a):[a ε n => P(a)] & ALL(b):[b ε n => Q(b)]
	       => ALL(a):ALL(b):[a ε n & b ε n => P(a) & Q(b)]
	
	Suppose...

	19	ALL(a):[a ε n => P(a)] & ALL(b):[b ε n => Q(b)]
		Premise

	Split premise

	20	ALL(a):[a ε n => P(a)]
		Split, 19

	21	ALL(b):[b ε n => Q(b)]
		Split, 19

		Prove: ALL(a):ALL(b):[a ε n & b ε n => P(a) & Q(b)]
		
		Suppose...

		22	x ε n & y ε n
			Premise

		23	x ε n
			Split, 22

		24	y ε n
			Split, 22

		Apply premise (line 20) for a=x

		25	x ε n => P(x)
			U Spec, 20

		Apply detachment

		26	P(x)
			Detach, 25, 23

		Apply premise (line 21) for b=y

		27	y ε n => Q(y)
			U Spec, 21

		Apply detachment

		28	Q(y)
			Detach, 27, 24

		Join results

		29	P(x) & Q(y)
			Join, 26, 28

	As Required:

	30	ALL(a):ALL(b):[a ε n & b ε n => P(a) & Q(b)]
		Conclusion, 22

"<="

As Required:

31	ALL(a):[a ε n => P(a)] & ALL(b):[b ε n => Q(b)]
	=> ALL(a):ALL(b):[a ε n & b ε n => P(a) & Q(b)]
	Conclusion, 19

Join results

32	[ALL(a):ALL(b):[a ε n & b ε n => P(a) & Q(b)]
	=> ALL(a):[a ε n => P(a)] & ALL(b):[b ε n => Q(b)]]
	& [ALL(a):[a ε n => P(a)] & ALL(b):[b ε n => Q(b)]
	=> ALL(a):ALL(b):[a ε n & b ε n => P(a) & Q(b)]]
	Join, 18, 31

As Required:

33	ALL(a):ALL(b):[a ε n & b ε n => P(a) & Q(b)]
	<=> ALL(a):[a ε n => P(a)] & ALL(b):[b ε n => Q(b)]
	Iff-And, 32