This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem r19.29

Description: Restricted quantifier version of 19.29 . See also r19.29r . (Contributed by NM, 31-Aug-1999) (Proof shortened by Andrew Salmon, 30-May-2011) (Proof shortened by Wolf Lammen, 22-Dec-2024)

Ref Expression
Assertion r19.29 ⊢ ∀ x ∈ A φ ∧ ∃ x ∈ A ψ → ∃ x ∈ A φ ∧ ψ

Proof

Step Hyp Ref Expression
1 ibar ⊢ φ → ψ ↔ φ ∧ ψ
2 1 ralrexbid ⊢ ∀ x ∈ A φ → ∃ x ∈ A ψ ↔ ∃ x ∈ A φ ∧ ψ
3 2 biimpa ⊢ ∀ x ∈ A φ ∧ ∃ x ∈ A ψ → ∃ x ∈ A φ ∧ ψ