Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Restricted quantification
Restricted universal and existential quantification
nrexdv
Metamath Proof Explorer
Description: Deduction adding restricted existential quantifier to negated wff.
(Contributed by NM , 16-Oct-2003) (Proof shortened by Wolf Lammen , 5-Jan-2020)
Ref
Expression
Hypothesis
nrexdv.1
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝜓 )
Assertion
nrexdv
⊢ ( 𝜑 → ¬ ∃ 𝑥 ∈ 𝐴 𝜓 )
Proof
Step
Hyp
Ref
Expression
1
nrexdv.1
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝜓 )
2
1
ralrimiva
⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ¬ 𝜓 )
3
ralnex
⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃ 𝑥 ∈ 𝐴 𝜓 )
4
2 3
sylib
⊢ ( 𝜑 → ¬ ∃ 𝑥 ∈ 𝐴 𝜓 )