Theorem nex 1807

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

Syntax hints:  ¬ wn 3  ∃wex 1786

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

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  ru  3721  ruOLD  3722  noel  4266  uni0  4866  axnulALT  5226  vnex  5239  notzfaus  5292  dtrucor2  5301  opelopabsb  5472  0nelopab  5507  0nelxp  5652  0xp  5717  xp0  5718  dm0  5862  cnv0  6090  cnv0OLD  6091  co02  6212  dffv3  6823  mpo0  7441  canth2  9058  snnen2o  9145  1sdom2dom  9154  brdom3  10441  ruc  16201  join0  18360  meet0  18361  0g0  18623  ustn0  24204  bnj1523  35253  axnulALT2  35264  linedegen  36371  nexntru  36632  nexfal  36633  unqsym1  36653  elttcirr  36759  bj-dtrucor2v  37170  bj-ru1  37296  bj-0nelsngl  37324  bj-ccinftydisj  37573  disjALTV0  39221  dtrucor3  49289