Theorem rexcomf

Description: Commutation of restricted existential quantifiers. For a version based on fewer axioms see rexcom . (Contributed by Mario Carneiro, 14-Oct-2016)

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

Proof

Step	Hyp	Ref	Expression
1		ralcomf.1	|- F/_ y A
2		ralcomf.2	|- F/_ x B
3		ancom	|- ( ( x e. A /\ y e. B ) <-> ( y e. B /\ x e. A ) )
4	3	anbi1i	|- ( ( ( x e. A /\ y e. B ) /\ ph ) <-> ( ( y e. B /\ x e. A ) /\ ph ) )
5	4	2exbii	|- ( E. x E. y ( ( x e. A /\ y e. B ) /\ ph ) <-> E. x E. y ( ( y e. B /\ x e. A ) /\ ph ) )
6		excom	|- ( E. x E. y ( ( y e. B /\ x e. A ) /\ ph ) <-> E. y E. x ( ( y e. B /\ x e. A ) /\ ph ) )
7	5 6	bitri	|- ( E. x E. y ( ( x e. A /\ y e. B ) /\ ph ) <-> E. y E. x ( ( y e. B /\ x e. A ) /\ ph ) )
8	1	r2exf	|- ( E. x e. A E. y e. B ph <-> E. x E. y ( ( x e. A /\ y e. B ) /\ ph ) )
9	2	r2exf	|- ( E. y e. B E. x e. A ph <-> E. y E. x ( ( y e. B /\ x e. A ) /\ ph ) )
10	7 8 9	3bitr4i	|- ( E. x e. A E. y e. B ph <-> E. y e. B E. x e. A ph )