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

Theorem nex 1632
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 1619 . 2  |-  ( A. x  -.  ph  <->  -.  E. x ph )
2 nex.1 . 2  |-  -.  ph
31, 2mpgbi 1626 1  |-  -.  E. x ph
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   E.wex 1617
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623
This theorem depends on definitions:  df-bi 185  df-ex 1618
This theorem is referenced by:  ru  3323  axnulALT  4566  notzfaus  4612  dtrucor2  4671  opelopabsb  4746  0nelxp  5016  0xp  5069  dm0  5205  co02  5504  dffv3  5844  mpt20  6340  canth2  7663  brdom3  8897  ruc  14060  meet0  15966  join0  15967  0g0  16089  ustn0  20889  linedegen  30021  nextnt  30098  nextf  30099  unqsym1  30118  amosym1  30119  subsym1  30120  bnj1523  34528  bj-dtrucor2v  34788  bj-ru1  34902  bj-0nelsngl  34930  bj-ccinftydisj  35016
  Copyright terms: Public domain W3C validator