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	⊢ Ⅎ 𝑦 𝐴
Assertion	rexcom4f	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 𝜑 ↔ ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		ralcom4f.1	⊢ Ⅎ 𝑦 𝐴
2		nfcv	⊢ Ⅎ 𝑥 V
3	1 2	rexcomf	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ V 𝜑 ↔ ∃ 𝑦 ∈ V ∃ 𝑥 ∈ 𝐴 𝜑 )
4		rexv	⊢ ( ∃ 𝑦 ∈ V 𝜑 ↔ ∃ 𝑦 𝜑 )
5	4	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ V 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 𝜑 )
6		rexv	⊢ ( ∃ 𝑦 ∈ V ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 𝜑 )
7	3 5 6	3bitr3i	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 𝜑 ↔ ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 𝜑 )