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

Theorem nex 1800
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 1781 . 2 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
2 nex.1 . 2 ¬ 𝜑
31, 2mpgbi 1798 1 ¬ ∃𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wex 1779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795
This theorem depends on definitions:  df-bi 207  df-ex 1780
This theorem is referenced by:  ru  3786  ruOLD  3787  noel  4338  axnulALT  5304  notzfaus  5363  dtrucor2  5372  opelopabsb  5535  0nelopab  5572  0nelxp  5719  0xp  5784  dm0  5931  cnv0  6160  co02  6280  dffv3  6902  mpo0  7518  canth2  9170  snnen2o  9273  1sdom2dom  9283  brdom3  10568  ruc  16279  join0  18450  meet0  18451  0g0  18677  ustn0  24229  bnj1523  35085  linedegen  36144  nexntru  36405  nexfal  36406  unqsym1  36426  bj-dtrucor2v  36818  bj-ru1  36944  bj-0nelsngl  36972  bj-ccinftydisj  37214  disjALTV0  38755  dtrucor3  48719
  Copyright terms: Public domain W3C validator