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

Theorem nex 1795
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 1776 . 2 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
2 nex.1 . 2 ¬ 𝜑
31, 2mpgbi 1793 1 ¬ ∃𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wex 1774
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790
This theorem depends on definitions:  df-bi 206  df-ex 1775
This theorem is referenced by:  ru  3773  ruOLD  3774  noel  4330  noelOLD  4331  axnulALT  5301  notzfaus  5359  dtrucor2  5368  opelopabsb  5528  0nelopab  5565  0nelxp  5708  0xp  5772  dm0  5919  cnv0  6144  co02  6263  dffv3  6889  mpo0  7502  canth2  9160  snnen2o  9264  1sdom2dom  9274  brdom3  10562  ruc  16240  join0  18425  meet0  18426  0g0  18652  ustn0  24213  bnj1523  34929  linedegen  35980  nexntru  36129  nexfal  36130  unqsym1  36150  bj-dtrucor2v  36535  bj-ru1  36663  bj-0nelsngl  36691  bj-ccinftydisj  36933  disjALTV0  38465  dtrucor3  48222
  Copyright terms: Public domain W3C validator