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 rexlimi
Description: Restricted quantifier version of exlimi . For a version based on
fewer axioms see rexlimiv . (Contributed by NM , 30-Nov-2003) (Proof
shortened by Andrew Salmon , 30-May-2011)
Ref
Expression
Hypotheses
rexlimi.1 ⊢ Ⅎ 𝑥 𝜓
rexlimi.2 ⊢ ( 𝑥 ∈ 𝐴 → ( 𝜑 → 𝜓 ) )
Assertion
rexlimi ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 → 𝜓 )
Proof
Step
Hyp
Ref
Expression
1
rexlimi.1 ⊢ Ⅎ 𝑥 𝜓
2
rexlimi.2 ⊢ ( 𝑥 ∈ 𝐴 → ( 𝜑 → 𝜓 ) )
3
2
rgen ⊢ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 )
4
1
r19.23 ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 → 𝜓 ) )
5
3 4
mpbi ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 → 𝜓 )