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

Theorem nex 1844
Description: Generalization rule for negated wff. (Contributed by NM, 18-May-1994.)
Hypothesis
Ref Expression
nex.1 ¬ 𝜑
Assertion
Ref Expression
nex ¬ ∃𝑥𝜑

Proof of Theorem nex
StepHypRef Expression
1 alnex 1825 . 2 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
2 nex.1 . 2 ¬ 𝜑
31, 2mpgbi 1842 1 ¬ ∃𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wex 1823
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839
This theorem depends on definitions:  df-bi 199  df-ex 1824
This theorem is referenced by:  ru  3650  noel  4145  axnulALT  5023  notzfaus  5074  dtrucor2  5084  opelopabsb  5222  0nelxp  5389  0xp  5447  dm0  5584  cnv0  5790  co02  5903  dffv3  6442  mpt20  7002  canth2  8401  brdom3  9685  ruc  15376  meet0  17523  join0  17524  0g0  17649  ustn0  22432  bnj1523  31738  linedegen  32839  nexntru  32987  nexfal  32988  unqsym1  33007  amosym1  33008  subsym1  33009  bj-dtrucor2v  33377  bj-ru1  33506  bj-0nelsngl  33531  bj-ccinftydisj  33690  nsb  38102
  Copyright terms: Public domain W3C validator