Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nex Structured version   Visualization version   GIF version

Theorem nex 1722
 Description: Generalization rule for negated wff. (Contributed by NM, 18-May-1994.)
Hypothesis
Ref Expression
nex.1 ¬ 𝜑
Assertion
Ref Expression
nex ¬ ∃𝑥𝜑

Proof of Theorem nex
StepHypRef Expression
1 alnex 1697 . 2 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
2 nex.1 . 2 ¬ 𝜑
31, 2mpgbi 1716 1 ¬ ∃𝑥𝜑
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3  ∃wex 1695 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713 This theorem depends on definitions:  df-bi 196  df-ex 1696 This theorem is referenced by:  ru  3401  axnulALT  4715  notzfaus  4766  dtrucor2  4828  opelopabsb  4910  0nelxp  5067  0nelxpOLD  5068  0xp  5122  dm0  5260  cnv0  5454  co02  5566  dffv3  6099  mpt20  6623  canth2  7998  brdom3  9231  ruc  14811  meet0  16960  join0  16961  0g0  17086  ustn0  21834  bnj1523  30393  linedegen  31420  nextnt  31574  nextf  31575  unqsym1  31594  amosym1  31595  subsym1  31596  bj-dtrucor2v  31989  bj-ru1  32125  bj-0nelsngl  32152  bj-ccinftydisj  32277
 Copyright terms: Public domain W3C validator