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

Theorem nex 1672
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 1659 . 2  |-  ( A. x  -.  ph  <->  -.  E. x ph )
2 nex.1 . 2  |-  -.  ph
31, 2mpgbi 1666 1  |-  -.  E. x ph
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   E.wex 1657
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663
This theorem depends on definitions:  df-bi 188  df-ex 1658
This theorem is referenced by:  ru  3298  axnulALT  4552  notzfaus  4599  dtrucor2  4655  opelopabsb  4730  0nelxp  4881  0xp  4934  dm0  5067  co02  5368  dffv3  5877  mpt20  6375  canth2  7734  brdom3  8963  ruc  14294  meet0  16382  join0  16383  0g0  16505  ustn0  21233  bnj1523  29888  linedegen  30915  nextnt  31070  nextf  31071  unqsym1  31090  amosym1  31091  subsym1  31092  bj-dtrucor2v  31386  bj-ru1  31506  bj-0nelsngl  31533  bj-ccinftydisj  31619
  Copyright terms: Public domain W3C validator