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

Theorem nex 1728
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 1703 . 2 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
2 nex.1 . 2 ¬ 𝜑
31, 2mpgbi 1722 1 ¬ ∃𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wex 1701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719
This theorem depends on definitions:  df-bi 197  df-ex 1702
This theorem is referenced by:  ru  3420  axnulALT  4752  notzfaus  4805  dtrucor2  4867  opelopabsb  4950  0nelxp  5108  0nelxpOLD  5109  0xp  5165  dm0  5304  cnv0  5499  co02  5613  dffv3  6149  mpt20  6685  canth2  8064  brdom3  9301  ruc  14904  meet0  17065  join0  17066  0g0  17191  ustn0  21943  bnj1523  30874  linedegen  31919  nextnt  32073  nextf  32074  unqsym1  32093  amosym1  32094  subsym1  32095  bj-dtrucor2v  32471  bj-ru1  32607  bj-0nelsngl  32633  bj-ccinftydisj  32760
  Copyright terms: Public domain W3C validator