Metamath Proof Explorer

Theorem rexcom4a

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

Ref Expression
Assertion rexcom4a ⊢ ∃ x ∃ y ∈ A φ ∧ ψ ↔ ∃ y ∈ A φ ∧ ∃ x ψ

Proof

Step Hyp Ref Expression
1 rexcom4 ⊢ ∃ y ∈ A ∃ x φ ∧ ψ ↔ ∃ x ∃ y ∈ A φ ∧ ψ
2 19.42v ⊢ ∃ x φ ∧ ψ ↔ φ ∧ ∃ x ψ
3 2 rexbii ⊢ ∃ y ∈ A ∃ x φ ∧ ψ ↔ ∃ y ∈ A φ ∧ ∃ x ψ
4 1 3 bitr3i ⊢ ∃ x ∃ y ∈ A φ ∧ ψ ↔ ∃ y ∈ A φ ∧ ∃ x ψ