Theorem rexcom4a

Description: Specialized existential commutation lemma. (Contributed by Jeff Madsen, 1-Jun-2011)

	Ref	Expression
Assertion	rexcom4a	⊢ ( ∃ 𝑥 ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ ∃ 𝑥 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		rexcom4	⊢ ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑥 ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) )
2		19.42v	⊢ ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ∃ 𝑥 𝜓 ) )
3	2	rexbii	⊢ ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ ∃ 𝑥 𝜓 ) )
4	1 3	bitr3i	⊢ ( ∃ 𝑥 ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ ∃ 𝑥 𝜓 ) )