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

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

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 207  df-ex 1782

This theorem is referenced by:  ru  3726  ruOLD  3727  noel  4278  uni0  4878  axnulALT  5239  vnex  5252  notzfaus  5305  dtrucor2  5314  opelopabsb  5485  0nelopab  5520  0nelxp  5665  0xp  5730  xp0  5731  dm0  5875  cnv0  6103  cnv0OLD  6104  co02  6225  dffv3  6836  mpo0  7452  canth2  9068  snnen2o  9155  1sdom2dom  9164  brdom3  10450  ruc  16210  join0  18369  meet0  18370  0g0  18632  ustn0  24186  bnj1523  35213  axnulALT2  35224  linedegen  36325  nexntru  36586  nexfal  36587  unqsym1  36607  elttcirr  36713  bj-dtrucor2v  37124  bj-ru1  37250  bj-0nelsngl  37278  bj-ccinftydisj  37527  disjALTV0  39175  dtrucor3  49274