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

Theorem nex 1729
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 1704 . 2 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
2 nex.1 . 2 ¬ 𝜑
31, 2mpgbi 1723 1 ¬ ∃𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wex 1702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720
This theorem depends on definitions:  df-bi 197  df-ex 1703
This theorem is referenced by:  ru  3428  axnulALT  4778  notzfaus  4831  dtrucor2  4892  opelopabsb  4975  0nelxp  5133  0nelxpOLD  5134  0xp  5189  dm0  5328  cnv0  5523  co02  5637  dffv3  6174  mpt20  6710  canth2  8098  brdom3  9335  ruc  14953  meet0  17118  join0  17119  0g0  17244  ustn0  22005  bnj1523  31113  linedegen  32225  nextnt  32379  nextf  32380  unqsym1  32399  amosym1  32400  subsym1  32401  bj-dtrucor2v  32776  bj-ru1  32908  bj-0nelsngl  32934  bj-ccinftydisj  33071
  Copyright terms: Public domain W3C validator