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  5261  vnex  5274  notsep  5328  dtrucor2  5337  opelopabsb  5508  0nelopab  5544  0nelxp  5689  0xp  5754  xp0  5755  cnv0  5863  cnv0OLD  5864  dm0  5904  co02  6257  dffv3  6874  mpo0  7498  canth2  9128  snnen2o  9215  1sdom2dom  9224  brdom3  10531  ruc  16331  join0  18491  meet0  18492  0g0  18757  ustn0  24447  bnj1523  35580  axnulALT2  35590  linedegen  36723  nexntru  37023  nexfal  37024  unqsym1  37044  elttcirr  37150  bj-dtrucor2v  37560  bj-ru1  37687  bj-0nelsngl  37715  bj-ccinftydisj  37965  disjALTV0  39602  dtrucor3  49727