Theorem nex 1833

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

This proof depends on syntax axioms:  ¬ wn 3  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  ru  3738  noel  4284  uni0  4896  axnulALT  5258  vnex  5271  notsep  5325  dtrucor2  5334  opelopabsb  5504  0nelopab  5540  0nelxp  5685  0xp  5750  xp0  5751  cnv0  5861  cnv0OLD  5862  dm0  5902  co02  6261  dffv3  6879  mpo0  7503  canth2  9142  snnen2o  9229  1sdom2dom  9238  brdom3  10600  ruc  16404  join0  18570  meet0  18571  0g0  18837  ustn0  24533  bnj1523  35694  axnulALT2  35704  linedegen  36888  nexntru  37172  nexfal  37173  unqsym1  37193  elttcirr  37299  bj-dtrucor2v  37709  bj-ru1  37836  bj-0nelsngl  37864  bj-ccinftydisj  38114  disjALTV0  39766  dtrucor3  49878