Theorem rexcom13

Description: Swap first and third restricted existential quantifiers. (Contributed by NM, 8-Apr-2015)

	Ref	Expression
Assertion	rexcom13	$$⊢\exists x\in A\exists y\in B\exists z\in C\phi \leftrightarrow \exists z\in C\exists y\in B\exists x\in A\phi$$

Proof

Step	Hyp	Ref	Expression
1		rexcom	$$⊢\exists x\in A\exists y\in B\exists z\in C\phi \leftrightarrow \exists y\in B\exists x\in A\exists z\in C\phi$$
2		rexcom	$$⊢\exists x\in A\exists z\in C\phi \leftrightarrow \exists z\in C\exists x\in A\phi$$
3	2	rexbii	$$⊢\exists y\in B\exists x\in A\exists z\in C\phi \leftrightarrow \exists y\in B\exists z\in C\exists x\in A\phi$$
4		rexcom	$$⊢\exists y\in B\exists z\in C\exists x\in A\phi \leftrightarrow \exists z\in C\exists y\in B\exists x\in A\phi$$
5	1 3 4	3bitri	$$⊢\exists x\in A\exists y\in B\exists z\in C\phi \leftrightarrow \exists z\in C\exists y\in B\exists x\in A\phi$$