This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality Restricted quantification Restricted universal and existential quantification 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 ⊢ Ⅎ 𝑥 𝜓
Assertion
r19.23 ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 → 𝜓 ) )
Proof
Step
Hyp
Ref
Expression
1
r19.23.1 ⊢ Ⅎ 𝑥 𝜓
2
r19.23t ⊢ ( Ⅎ 𝑥 𝜓 → ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 → 𝜓 ) ) )
3
1 2
ax-mp ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 → 𝜓 ) )