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

Theorem nex 1561
Description: Generalization rule for negated wff. (Contributed by NM, 18-May-1994.)
Hypothesis
Ref Expression
nex.1  |-  -.  ph
Assertion
Ref Expression
nex  |-  -.  E. x ph

Proof of Theorem nex
StepHypRef Expression
1 alnex 1549 . 2  |-  ( A. x  -.  ph  <->  -.  E. x ph )
2 nex.1 . 2  |-  -.  ph
31, 2mpgbi 1555 1  |-  -.  E. x ph
Colors of variables: wff set class
Syntax hints:   -. wn 3   E.wex 1547
This theorem is referenced by:  ru  3128  axnulALT  4304  notzfaus  4342  dtrucor2  4366  opelopabsb  4433  0nelxp  4873  xp0r  4923  dm0  5050  co02  5350  dffv3  5691  mpt20  6394  canth2  7227  brdom3  8370  ruc  12805  0g0  14672  ustn0  18211  linedegen  25989  nextnt  26067  nextf  26068  unqsym1  26087  amosym1  26088  subsym1  26089  bnj1523  29158
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator