Theorem 2ex2rexrot

Description: Rotate two existential quantifiers and two restricted existential quantifiers. (Contributed by AV, 9-Nov-2023)

	Ref	Expression
Assertion	2ex2rexrot	$$⊢\exists x\exists y\exists z\in A\exists w\in B\phi \leftrightarrow \exists z\in A\exists w\in B\exists x\exists y\phi$$

Proof

Step	Hyp	Ref	Expression
1		rexcom4	$$⊢\exists w\in B\exists x\exists y\phi \leftrightarrow \exists x\exists w\in B\exists y\phi$$
2	1	rexbii	$$⊢\exists z\in A\exists w\in B\exists x\exists y\phi \leftrightarrow \exists z\in A\exists x\exists w\in B\exists y\phi$$
3		rexcom4	$$⊢\exists z\in A\exists x\exists w\in B\exists y\phi \leftrightarrow \exists x\exists z\in A\exists w\in B\exists y\phi$$
4		rexcom4	$$⊢\exists w\in B\exists y\phi \leftrightarrow \exists y\exists w\in B\phi$$
5	4	rexbii	$$⊢\exists z\in A\exists w\in B\exists y\phi \leftrightarrow \exists z\in A\exists y\exists w\in B\phi$$
6		rexcom4	$$⊢\exists z\in A\exists y\exists w\in B\phi \leftrightarrow \exists y\exists z\in A\exists w\in B\phi$$
7	5 6	bitri	$$⊢\exists z\in A\exists w\in B\exists y\phi \leftrightarrow \exists y\exists z\in A\exists w\in B\phi$$
8	7	exbii	$$⊢\exists x\exists z\in A\exists w\in B\exists y\phi \leftrightarrow \exists x\exists y\exists z\in A\exists w\in B\phi$$
9	2 3 8	3bitrri	$$⊢\exists x\exists y\exists z\in A\exists w\in B\phi \leftrightarrow \exists z\in A\exists w\in B\exists x\exists y\phi$$