Theorem nex 1796

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

Syntax hints:  ¬ wn 3  ∃wex 1775

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

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

This theorem is referenced by:  ru  3788  ruOLD  3789  noel  4343  axnulALT  5309  notzfaus  5368  dtrucor2  5377  opelopabsb  5539  0nelopab  5576  0nelxp  5722  0xp  5786  dm0  5933  cnv0  6162  co02  6281  dffv3  6902  mpo0  7517  canth2  9168  snnen2o  9270  1sdom2dom  9280  brdom3  10565  ruc  16275  join0  18462  meet0  18463  0g0  18689  ustn0  24244  bnj1523  35063  linedegen  36124  nexntru  36386  nexfal  36387  unqsym1  36407  bj-dtrucor2v  36799  bj-ru1  36925  bj-0nelsngl  36953  bj-ccinftydisj  37195  disjALTV0  38735  dtrucor3  48647