Theorem nex 1803

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

Syntax hints:  ¬ wn 3  ∃wex 1782

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

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

This theorem is referenced by:  ru  3777  noel  4331  noelOLD  4332  axnulALT  5305  notzfaus  5362  dtrucor2  5371  opelopabsb  5531  0nelopab  5568  0nelxp  5711  0xp  5775  dm0  5921  cnv0  6141  co02  6260  dffv3  6888  mpo0  7494  canth2  9130  snnen2o  9237  1sdom2dom  9247  brdom3  10523  ruc  16186  join0  18358  meet0  18359  0g0  18583  ustn0  23725  bnj1523  34082  linedegen  35115  nexntru  35289  nexfal  35290  unqsym1  35310  bj-dtrucor2v  35695  bj-ru1  35824  bj-0nelsngl  35852  bj-ccinftydisj  36094  disjALTV0  37624  dtrucor3  47484