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

Theorem nex 1879
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 1854 . 2 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
2 nex.1 . 2 ¬ 𝜑
31, 2mpgbi 1873 1 ¬ ∃𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wex 1852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870
This theorem depends on definitions:  df-bi 197  df-ex 1853
This theorem is referenced by:  ru  3586  axnulALT  4921  notzfaus  4971  dtrucor2  5029  opelopabsb  5118  0nelxp  5283  0nelxpOLD  5284  0xp  5339  dm0  5477  cnv0  5676  co02  5793  dffv3  6328  mpt20  6872  canth2  8269  brdom3  9552  ruc  15178  meet0  17345  join0  17346  0g0  17471  ustn0  22244  bnj1523  31477  linedegen  32587  nextnt  32741  nextf  32742  unqsym1  32761  amosym1  32762  subsym1  32763  bj-dtrucor2v  33137  bj-ru1  33265  bj-0nelsngl  33290  bj-ccinftydisj  33437
  Copyright terms: Public domain W3C validator