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

Metamath Proof Explorer

Theorem nex

Description: Generalization rule for negated wff. (Contributed by NM, 18-May-1994)

Ref Expression
Hypothesis nex.1 ⊢ ¬ 𝜑
Assertion nex ¬ ∃ 𝑥 𝜑

Proof

Step Hyp Ref Expression
1 nex.1 ⊢ ¬ 𝜑
2 alnex ⊢ ( ∀ 𝑥 ¬ 𝜑 ↔ ¬ ∃ 𝑥 𝜑 )
3 2 1 mpgbi ⊢ ¬ ∃ 𝑥 𝜑