Theorem rexcomOLD

Description: Obsolete version of rexcom as of 26-Aug-2023. Commutation of restricted existential quantifiers. (Contributed by NM, 19-Nov-1995) (Revised by Mario Carneiro, 14-Oct-2016) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	rexcomOLD	$$⊢\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		ancom	$$⊢\left(x\in A\wedge y\in B\right)\leftrightarrow \left(y\in B\wedge x\in A\right)$$
2	1	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)$$
3	2	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)$$
4		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)$$
5	3 4	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)$$
6		r2ex	$$⊢\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)$$
7		r2ex	$$⊢\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)$$
8	5 6 7	3bitr4i	$$⊢\exists x\in A\exists y\in B\phi \leftrightarrow \exists y\in B\exists x\in A\phi$$