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

Theorem nex 1555
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 1543 . 2  |-  ( A. x  -.  ph  <->  -.  E. x ph )
2 nex.1 . 2  |-  -.  ph
31, 2mpgbi 1549 1  |-  -.  E. x ph
Colors of variables: wff set class
Syntax hints:   -. wn 3   E.wex 1541
This theorem is referenced by:  ru  3066  axnulALT  4228  notzfaus  4266  dtrucor2  4290  opelopabsb  4357  0nelxp  4799  xp0r  4850  dm0  4974  co02  5268  dffv3  5604  mpt20  6286  canth2  7102  brdom3  8243  ruc  12618  0g0  14485  ustn0  23524  linedegen  25325  nextnt  25403  nextf  25404  unqsym1  25423  amosym1  25424  subsym1  25425  bnj1523  28863
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546
This theorem depends on definitions:  df-bi 177  df-ex 1542
  Copyright terms: Public domain W3C validator