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

Theorem nex 1802
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 1783 . 2 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
2 nex.1 . 2 ¬ 𝜑
31, 2mpgbi 1800 1 ¬ ∃𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wex 1781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797
This theorem depends on definitions:  df-bi 210  df-ex 1782
This theorem is referenced by:  ru  3719  noel  4247  axnulALT  5172  notzfaus  5227  notzfausOLD  5228  dtrucor2  5238  opelopabsb  5382  0nelxp  5553  0xp  5613  dm0  5754  cnv0  5966  co02  6080  dffv3  6641  mpo0  7218  canth2  8654  brdom3  9939  ruc  15588  meet0  17739  join0  17740  0g0  17866  ustn0  22826  bnj1523  32453  linedegen  33714  nexntru  33862  nexfal  33863  unqsym1  33883  amosym1  33884  subsym1  33885  bj-dtrucor2v  34252  bj-ru1  34375  bj-0nelsngl  34404  bj-ccinftydisj  34625  disjALTV0  36141  nsb  39387
  Copyright terms: Public domain W3C validator