Theorem nex 1799

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

Step	Hyp	Ref	Expression
1		alnex 1780	. 2 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
2		nex.1	. 2 ⊢ ¬ 𝜑
3	1, 2	mpgbi 1797	1 ⊢ ¬ ∃𝑥𝜑

Syntax hints:  ¬ wn 3  ∃wex 1778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794

This theorem depends on definitions:  df-bi 207  df-ex 1779

This theorem is referenced by:  ru  3761  ruOLD  3762  noel  4311  axnulALT  5272  notzfaus  5331  dtrucor2  5340  opelopabsb  5503  0nelopab  5540  0nelxp  5686  0xp  5751  dm0  5898  cnv0  6127  co02  6247  dffv3  6869  mpo0  7487  canth2  9139  snnen2o  9240  1sdom2dom  9250  brdom3  10535  ruc  16248  join0  18402  meet0  18403  0g0  18629  ustn0  24146  bnj1523  35031  linedegen  36090  nexntru  36351  nexfal  36352  unqsym1  36372  bj-dtrucor2v  36764  bj-ru1  36890  bj-0nelsngl  36918  bj-ccinftydisj  37160  disjALTV0  38701  dtrucor3  48672