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

Theorem nex 1542
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 1530 . 2  |-  ( A. x  -.  ph  <->  -.  E. x ph )
2 nex.1 . 2  |-  -.  ph
31, 2mpgbi 1536 1  |-  -.  E. x ph
Colors of variables: wff set class
Syntax hints:   -. wn 3   E.wex 1528
This theorem is referenced by:  ru  2990  axnulALT  4147  notzfaus  4185  dtrucor2  4209  opelopabsb  4275  0nelxp  4717  xp0r  4768  dm0  4892  co02  5186  dffv3  5521  mpt20  6199  canth2  7014  brdom3  8153  ruc  12521  0g0  14386  funpartfv  24483  linedegen  24766  nextnt  24844  nextf  24845  unqsym1  24864  amosym1  24865  subsym1  24866  bnj1523  29101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533
This theorem depends on definitions:  df-bi 177  df-ex 1529
  Copyright terms: Public domain W3C validator