Theorem rexcom4f

Description: Commutation of restricted and unrestricted existential quantifiers. (Contributed by NM, 12-Apr-2004) (Proof shortened by Andrew Salmon, 8-Jun-2011) (Revised by Thierry Arnoux, 8-Mar-2017)

	Ref	Expression
Hypothesis	ralcom4f.1	$$⊢\underset{\_}{Ⅎ}yA$$
Assertion	rexcom4f	$$⊢\exists x\in A\exists y\phi \leftrightarrow \exists y\exists x\in A\phi$$

Proof

Step	Hyp	Ref	Expression
1		ralcom4f.1	$$⊢\underset{\_}{Ⅎ}yA$$
2		nfcv	$$⊢\underset{\_}{Ⅎ}x\mathrm{V}$$
3	1 2	rexcomf	$$⊢\exists x\in A\exists y\in \mathrm{V}\phi \leftrightarrow \exists y\in \mathrm{V}\exists x\in A\phi$$
4		rexv	$$⊢\exists y\in \mathrm{V}\phi \leftrightarrow \exists y\phi$$
5	4	rexbii	$$⊢\exists x\in A\exists y\in \mathrm{V}\phi \leftrightarrow \exists x\in A\exists y\phi$$
6		rexv	$$⊢\exists y\in \mathrm{V}\exists x\in A\phi \leftrightarrow \exists y\exists x\in A\phi$$
7	3 5 6	3bitr3i	$$⊢\exists x\in A\exists y\phi \leftrightarrow \exists y\exists x\in A\phi$$