Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Restricted quantification
Restricted universal and existential quantification
r19.29af
Metamath Proof Explorer
Description: A commonly used pattern based on r19.29 . See r19.29a , r19.29an for a variant when x is disjoint from ph . (Contributed by Thierry Arnoux , 29-Nov-2017)
Ref
Expression
Hypotheses
r19.29af.0
⊢ Ⅎ 𝑥 𝜑
r19.29af.1
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜓 ) → 𝜒 )
r19.29af.2
⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 )
Assertion
r19.29af
⊢ ( 𝜑 → 𝜒 )
Proof
Step
Hyp
Ref
Expression
1
r19.29af.0
⊢ Ⅎ 𝑥 𝜑
2
r19.29af.1
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜓 ) → 𝜒 )
3
r19.29af.2
⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 )
4
nfv
⊢ Ⅎ 𝑥 𝜒
5
1 4 2 3
r19.29af2
⊢ ( 𝜑 → 𝜒 )