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

Theorem nex 1610
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 1598 . 2  |-  ( A. x  -.  ph  <->  -.  E. x ph )
2 nex.1 . 2  |-  -.  ph
31, 2mpgbi 1604 1  |-  -.  E. x ph
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   E.wex 1596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601
This theorem depends on definitions:  df-bi 185  df-ex 1597
This theorem is referenced by:  ru  3335  axnulALT  4580  notzfaus  4628  dtrucor2  4687  opelopabsb  4763  0nelxp  5033  0xp  5086  dm0  5222  co02  5527  dffv3  5868  mpt20  6362  canth2  7682  brdom3  8918  ruc  13854  meet0  15641  join0  15642  0g0  15764  ustn0  20591  linedegen  29720  nextnt  29797  nextf  29798  unqsym1  29817  amosym1  29818  subsym1  29819  bnj1523  33607  bj-dtrucor2v  33869  bj-ru1  33983  bj-0nelsngl  34011  bj-ccinftydisj  34089
  Copyright terms: Public domain W3C validator