Theorem rexcom

Description: Commutation of restricted existential quantifiers. (Contributed by NM, 19-Nov-1995) (Revised by Mario Carneiro, 14-Oct-2016) (Proof shortened by BJ, 26-Aug-2023)

	Ref	Expression
Assertion	rexcom	$$⊢\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		df-rex	$$⊢\exists y\in B\phi \leftrightarrow \exists y\left(y\in B\wedge \phi \right)$$
2	1	rexbii	$$⊢\exists x\in A\exists y\in B\phi \leftrightarrow \exists x\in A\exists y\left(y\in B\wedge \phi \right)$$
3		rexcom4	$$⊢\exists x\in A\exists y\left(y\in B\wedge \phi \right)\leftrightarrow \exists y\exists x\in A\left(y\in B\wedge \phi \right)$$
4		r19.42v	$$⊢\exists x\in A\left(y\in B\wedge \phi \right)\leftrightarrow \left(y\in B\wedge \exists x\in A\phi \right)$$
5	4	exbii	$$⊢\exists y\exists x\in A\left(y\in B\wedge \phi \right)\leftrightarrow \exists y\left(y\in B\wedge \exists x\in A\phi \right)$$
6		df-rex	$$⊢\exists y\in B\exists x\in A\phi \leftrightarrow \exists y\left(y\in B\wedge \exists x\in A\phi \right)$$
7	5 6	bitr4i	$$⊢\exists y\exists x\in A\left(y\in B\wedge \phi \right)\leftrightarrow \exists y\in B\exists x\in A\phi$$
8	2 3 7	3bitri	$$⊢\exists x\in A\exists y\in B\phi \leftrightarrow \exists y\in B\exists x\in A\phi$$