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

Theorem nex 1565
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 1553 . 2  |-  ( A. x  -.  ph  <->  -.  E. x ph )
2 nex.1 . 2  |-  -.  ph
31, 2mpgbi 1559 1  |-  -.  E. x ph
Colors of variables: wff set class
Syntax hints:   -. wn 3   E.wex 1551
This theorem is referenced by:  ru  3162  axnulALT  4339  notzfaus  4377  dtrucor2  4401  opelopabsb  4468  0nelxp  4909  xp0r  4959  dm0  5086  co02  5386  dffv3  5727  mpt20  6430  canth2  7263  brdom3  8411  ruc  12847  0g0  14714  ustn0  18255  linedegen  26082  nextnt  26160  nextf  26161  unqsym1  26180  amosym1  26181  subsym1  26182  bnj1523  29514
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556
This theorem depends on definitions:  df-bi 179  df-ex 1552
  Copyright terms: Public domain W3C validator