This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nrex

Description: Inference adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003)

Ref Expression
Hypothesis nrex.1 ⊢ ( 𝑥 ∈ 𝐴 → ¬ 𝜓 )
Assertion nrex ¬ ∃ 𝑥 ∈ 𝐴 𝜓

Proof

Step Hyp Ref Expression
1 nrex.1 ⊢ ( 𝑥 ∈ 𝐴 → ¬ 𝜓 )
2 1 rgen ⊢ ∀ 𝑥 ∈ 𝐴 ¬ 𝜓
3 ralnex ⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃ 𝑥 ∈ 𝐴 𝜓 )
4 2 3 mpbi ⊢ ¬ ∃ 𝑥 ∈ 𝐴 𝜓