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

Theorem nex 1806
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 1787 . 2 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
2 nex.1 . 2 ¬ 𝜑
31, 2mpgbi 1804 1 ¬ ∃𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wex 1785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801
This theorem depends on definitions:  df-bi 206  df-ex 1786
This theorem is referenced by:  ru  3718  noel  4269  noelOLD  4270  axnulALT  5231  notzfaus  5288  dtrucor2  5298  opelopabsb  5444  0nelopab  5479  0nelxp  5622  0xp  5683  dm0  5826  cnv0  6041  co02  6161  dffv3  6764  mpo0  7351  canth2  8882  brdom3  10268  ruc  15933  join0  18104  meet0  18105  0g0  18329  ustn0  23353  bnj1523  33030  linedegen  34424  nexntru  34572  nexfal  34573  unqsym1  34593  amosym1  34594  subsym1  34595  bj-dtrucor2v  34979  bj-ru1  35111  bj-0nelsngl  35140  bj-ccinftydisj  35363  disjALTV0  36841  dtrucor3  46096
  Copyright terms: Public domain W3C validator