Theorem nex 1830

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

Syntax hints:  ¬ wn 3  ∃wex 1809

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

This theorem depends on definitions:  df-bi 210  df-ex 1810

This theorem is referenced by:  ru  3744  noel  4292  uni0  4902  axnulALT  5268  vnex  5281  notsep  5336  dtrucor2  5345  opelopabsb  5516  0nelopab  5552  0nelxp  5697  0xp  5762  xp0  5763  cnv0  5871  cnv0OLD  5872  dm0  5912  co02  6264  dffv3  6879  mpo0  7497  canth2  9119  snnen2o  9206  1sdom2dom  9215  brdom3  10513  ruc  16300  join0  18460  meet0  18461  0g0  18723  ustn0  24359  bnj1523  35440  axnulALT2  35452  linedegen  36616  nexntru  36896  nexfal  36897  unqsym1  36917  elttcirr  37023  bj-dtrucor2v  37433  bj-ru1  37560  bj-0nelsngl  37588  bj-ccinftydisj  37838  disjALTV0  39484  dtrucor3  49560