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

Theorem nex 1682
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 1669 . 2  |-  ( A. x  -.  ph  <->  -.  E. x ph )
2 nex.1 . 2  |-  -.  ph
31, 2mpgbi 1676 1  |-  -.  E. x ph
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   E.wex 1667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673
This theorem depends on definitions:  df-bi 190  df-ex 1668
This theorem is referenced by:  ru  3234  axnulALT  4503  notzfaus  4551  dtrucor2  4607  opelopabsb  4684  0nelxp  4840  0xp  4893  dm0  5026  co02  5328  dffv3  5844  mpt20  6349  canth2  7712  brdom3  8943  ruc  14306  meet0  16394  join0  16395  0g0  16517  ustn0  21246  bnj1523  29886  linedegen  30916  nextnt  31071  nextf  31072  unqsym1  31091  amosym1  31092  subsym1  31093  bj-dtrucor2v  31418  bj-ru1  31540  bj-0nelsngl  31567  bj-ccinftydisj  31657
  Copyright terms: Public domain W3C validator