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

Metamath Proof Explorer

Theorem r19.23

Description: Restricted quantifier version of 19.23 . See r19.23v for a version requiring fewer axioms. (Contributed by NM, 22-Oct-2010) (Proof shortened by Mario Carneiro, 8-Oct-2016)

Ref Expression
Hypothesis r19.23.1 ⊢ Ⅎ x ψ
Assertion r19.23 ⊢ ∀ x ∈ A φ → ψ ↔ ∃ x ∈ A φ → ψ

Proof

Step Hyp Ref Expression
1 r19.23.1 ⊢ Ⅎ x ψ
2 r19.23t ⊢ Ⅎ x ψ → ∀ x ∈ A φ → ψ ↔ ∃ x ∈ A φ → ψ
3 1 2 ax-mp ⊢ ∀ x ∈ A φ → ψ ↔ ∃ x ∈ A φ → ψ