Theorem nex 1798

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

Syntax hints:  ¬ wn 3  ∃wex 1777

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

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

This theorem is referenced by:  ru  3802  ruOLD  3803  noel  4360  noelOLD  4361  axnulALT  5322  notzfaus  5381  dtrucor2  5390  opelopabsb  5549  0nelopab  5586  0nelxp  5734  0xp  5798  dm0  5945  cnv0  6172  co02  6291  dffv3  6916  mpo0  7535  canth2  9196  snnen2o  9300  1sdom2dom  9310  brdom3  10597  ruc  16291  join0  18475  meet0  18476  0g0  18702  ustn0  24250  bnj1523  35047  linedegen  36107  nexntru  36370  nexfal  36371  unqsym1  36391  bj-dtrucor2v  36783  bj-ru1  36909  bj-0nelsngl  36937  bj-ccinftydisj  37179  disjALTV0  38710  dtrucor3  48532