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

Theorem nex 1880
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 1855 . 2 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
2 nex.1 . 2 ¬ 𝜑
31, 2mpgbi 1874 1 ¬ ∃𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wex 1853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871
This theorem depends on definitions:  df-bi 197  df-ex 1854
This theorem is referenced by:  ru  3575  axnulALT  4939  notzfaus  4989  dtrucor2  5050  opelopabsb  5135  0nelxp  5300  0nelxpOLD  5301  0xp  5356  dm0  5494  cnv0  5693  co02  5810  dffv3  6348  mpt20  6890  canth2  8278  brdom3  9542  ruc  15171  meet0  17338  join0  17339  0g0  17464  ustn0  22225  bnj1523  31446  linedegen  32556  nextnt  32710  nextf  32711  unqsym1  32730  amosym1  32731  subsym1  32732  bj-dtrucor2v  33107  bj-ru1  33239  bj-0nelsngl  33265  bj-ccinftydisj  33411
  Copyright terms: Public domain W3C validator