Theorem nex 1801

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

Syntax hints:  ¬ wn 3  ∃wex 1780

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

This theorem depends on definitions:  df-bi 206  df-ex 1781

This theorem is referenced by:  ru  3726  noel  4277  noelOLD  4278  axnulALT  5248  notzfaus  5305  dtrucor2  5315  opelopabsb  5474  0nelopab  5511  0nelxp  5654  0xp  5716  dm0  5862  cnv0  6079  co02  6198  dffv3  6821  mpo0  7422  canth2  8995  snnen2o  9102  1sdom2dom  9112  brdom3  10385  ruc  16051  join0  18220  meet0  18221  0g0  18445  ustn0  23478  bnj1523  33350  linedegen  34541  nexntru  34689  nexfal  34690  unqsym1  34710  bj-dtrucor2v  35095  bj-ru1  35227  bj-0nelsngl  35255  bj-ccinftydisj  35497  disjALTV0  37029  dtrucor3  46504