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

Theorem nex 1674
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 1661 . 2  |-  ( A. x  -.  ph  <->  -.  E. x ph )
2 nex.1 . 2  |-  -.  ph
31, 2mpgbi 1668 1  |-  -.  E. x ph
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   E.wex 1659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665
This theorem depends on definitions:  df-bi 188  df-ex 1660
This theorem is referenced by:  ru  3304  axnulALT  4554  notzfaus  4600  dtrucor2  4656  opelopabsb  4731  0nelxp  4882  0xp  4935  dm0  5068  co02  5369  dffv3  5877  mpt20  6375  canth2  7731  brdom3  8954  ruc  14273  meet0  16334  join0  16335  0g0  16457  ustn0  21166  bnj1523  29668  linedegen  30695  nextnt  30850  nextf  30851  unqsym1  30870  amosym1  30871  subsym1  30872  bj-dtrucor2v  31167  bj-ru1  31287  bj-0nelsngl  31314  bj-ccinftydisj  31400
  Copyright terms: Public domain W3C validator