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
⊢ φ ∧ x ∈ A → ¬ ψ
Assertion
nrexdv
⊢ φ → ¬ ∃ x ∈ A ψ
Proof
Step
Hyp
Ref
Expression
1
nrexdv.1
⊢ φ ∧ x ∈ A → ¬ ψ
2
1
ralrimiva
⊢ φ → ∀ x ∈ A ¬ ψ
3
ralnex
⊢ ∀ x ∈ A ¬ ψ ↔ ¬ ∃ x ∈ A ψ
4
2 3
sylib
⊢ φ → ¬ ∃ x ∈ A ψ