Theorem nex 1827

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

Syntax hints:  ¬ wn 3  ∃wex 1806

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

This theorem depends on definitions:  df-bi 210  df-ex 1807

This theorem is referenced by:  ru  3752  noel  4299  uni0  4902  axnulALT  5266  vnex  5279  notzfaus  5332  dtrucor2  5341  opelopabsb  5512  0nelopab  5548  0nelxp  5693  0xp  5758  xp0  5759  cnv0  5867  cnv0OLD  5868  dm0  5908  co02  6259  dffv3  6875  mpo0  7493  canth2  9114  snnen2o  9201  1sdom2dom  9210  brdom3  10508  ruc  16295  join0  18455  meet0  18456  0g0  18718  ustn0  24343  bnj1523  35400  axnulALT2  35411  linedegen  36530  nexntru  36800  nexfal  36801  unqsym1  36821  elttcirr  36927  bj-dtrucor2v  37337  bj-ru1  37463  bj-0nelsngl  37491  bj-ccinftydisj  37740  disjALTV0  39388  dtrucor3  49455