Metamath Proof Explorer

Theorem r19.42v

Description: Restricted quantifier version of 19.42v (see also 19.42 ). (Contributed by NM, 27-May-1998)

Ref Expression
Assertion r19.42v ⊢ ∃ x ∈ A φ ∧ ψ ↔ φ ∧ ∃ x ∈ A ψ

Proof

Step Hyp Ref Expression
1 r19.41v ⊢ ∃ x ∈ A ψ ∧ φ ↔ ∃ x ∈ A ψ ∧ φ
2 ancom ⊢ φ ∧ ψ ↔ ψ ∧ φ
3 2 rexbii ⊢ ∃ x ∈ A φ ∧ ψ ↔ ∃ x ∈ A ψ ∧ φ
4 ancom ⊢ φ ∧ ∃ x ∈ A ψ ↔ ∃ x ∈ A ψ ∧ φ
5 1 3 4 3bitr4i ⊢ ∃ x ∈ A φ ∧ ψ ↔ φ ∧ ∃ x ∈ A ψ