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	$$⊢\underset{\_}{Ⅎ}yA$$
	ralcomf.2	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	rexcomf	$$⊢\exists x\in A\exists y\in B\phi \leftrightarrow \exists y\in B\exists x\in A\phi$$

Proof

Step	Hyp	Ref	Expression
1		ralcomf.1	$$⊢\underset{\_}{Ⅎ}yA$$
2		ralcomf.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		ancom	$$⊢\left(x\in A\wedge y\in B\right)\leftrightarrow \left(y\in B\wedge x\in A\right)$$
4	3	anbi1i	$$⊢\left(\left(x\in A\wedge y\in B\right)\wedge \phi \right)\leftrightarrow \left(\left(y\in B\wedge x\in A\right)\wedge \phi \right)$$
5	4	2exbii	$$⊢\exists x\exists y\left(\left(x\in A\wedge y\in B\right)\wedge \phi \right)\leftrightarrow \exists x\exists y\left(\left(y\in B\wedge x\in A\right)\wedge \phi \right)$$
6		excom	$$⊢\exists x\exists y\left(\left(y\in B\wedge x\in A\right)\wedge \phi \right)\leftrightarrow \exists y\exists x\left(\left(y\in B\wedge x\in A\right)\wedge \phi \right)$$
7	5 6	bitri	$$⊢\exists x\exists y\left(\left(x\in A\wedge y\in B\right)\wedge \phi \right)\leftrightarrow \exists y\exists x\left(\left(y\in B\wedge x\in A\right)\wedge \phi \right)$$
8	1	r2exf	$$⊢\exists x\in A\exists y\in B\phi \leftrightarrow \exists x\exists y\left(\left(x\in A\wedge y\in B\right)\wedge \phi \right)$$
9	2	r2exf	$$⊢\exists y\in B\exists x\in A\phi \leftrightarrow \exists y\exists x\left(\left(y\in B\wedge x\in A\right)\wedge \phi \right)$$
10	7 8 9	3bitr4i	$$⊢\exists x\in A\exists y\in B\phi \leftrightarrow \exists y\in B\exists x\in A\phi$$