Theorem nex 1819

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 1800	. 2 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
2		nex.1	. 2 ⊢ ¬ 𝜑
3	1, 2	mpgbi 1817	1 ⊢ ¬ ∃𝑥𝜑

Syntax hints:  ¬ wn 3  ∃wex 1798

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

This theorem depends on definitions:  df-bi 209  df-ex 1799

This theorem is referenced by:  ru  3741  noel  4288  uni0  4891  axnulALT  5251  vnex  5264  notzfaus  5317  dtrucor2  5326  opelopabsb  5497  0nelopab  5532  0nelxp  5677  0xp  5742  xp0  5743  cnv0  5851  cnv0OLD  5852  dm0  5892  co02  6243  dffv3  6858  mpo0  7476  canth2  9096  snnen2o  9183  1sdom2dom  9192  brdom3  10479  ruc  16266  join0  18426  meet0  18427  0g0  18689  ustn0  24269  bnj1523  35327  axnulALT2  35338  linedegen  36454  nexntru  36725  nexfal  36726  unqsym1  36746  elttcirr  36852  bj-dtrucor2v  37263  bj-ru1  37389  bj-0nelsngl  37417  bj-ccinftydisj  37666  disjALTV0  39314  dtrucor3  49381