Theorem ralcomf

Description: Commutation of restricted universal quantifiers. (Contributed by Mario Carneiro, 14-Oct-2016)

	Ref	Expression
Hypotheses	ralcomf.1	|- F/_ y A
	ralcomf.2	|- F/_ x B
Assertion	ralcomf	|- ( A. x e. A A. y e. B ph <-> A. y e. B A. x e. A ph )

Proof

Step	Hyp	Ref	Expression
1		ralcomf.1	|- F/_ y A
2		ralcomf.2	|- F/_ x B
3		ancomst	|- ( ( ( x e. A /\ y e. B ) -> ph ) <-> ( ( y e. B /\ x e. A ) -> ph ) )
4	3	2albii	|- ( A. x A. y ( ( x e. A /\ y e. B ) -> ph ) <-> A. x A. y ( ( y e. B /\ x e. A ) -> ph ) )
5		alcom	|- ( A. x A. y ( ( y e. B /\ x e. A ) -> ph ) <-> A. y A. x ( ( y e. B /\ x e. A ) -> ph ) )
6	4 5	bitri	|- ( A. x A. y ( ( x e. A /\ y e. B ) -> ph ) <-> A. y A. x ( ( y e. B /\ x e. A ) -> ph ) )
7	1	r2alf	|- ( A. x e. A A. y e. B ph <-> A. x A. y ( ( x e. A /\ y e. B ) -> ph ) )
8	2	r2alf	|- ( A. y e. B A. x e. A ph <-> A. y A. x ( ( y e. B /\ x e. A ) -> ph ) )
9	6 7 8	3bitr4i	|- ( A. x e. A A. y e. B ph <-> A. y e. B A. x e. A ph )