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

Theorem nex 1882
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 1861 . 2 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
2 nex.1 . 2 ¬ 𝜑
31, 2mpgbi 1880 1 ¬ ∃𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wex 1859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877
This theorem depends on definitions:  df-bi 198  df-ex 1860
This theorem is referenced by:  ru  3626  axnulALT  4975  notzfaus  5026  dtrucor2  5036  opelopabsb  5174  0nelxp  5338  0xp  5395  dm0  5534  cnv0  5740  co02  5857  dffv3  6398  mpt20  6949  canth2  8346  brdom3  9629  ruc  15186  meet0  17336  join0  17337  0g0  17462  ustn0  22231  bnj1523  31456  linedegen  32565  nextnt  32715  nextf  32716  unqsym1  32735  amosym1  32736  subsym1  32737  bj-dtrucor2v  33109  bj-ru1  33238  bj-0nelsngl  33263  bj-ccinftydisj  33411
  Copyright terms: Public domain W3C validator