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  6262  dffv3  6881  mpo0  7505  canth2  9149  snnen2o  9236  1sdom2dom  9245  brdom3  10607  ruc  16411  join0  18577  meet0  18578  0g0  18844  ustn0  24540  bnj1523  35701  axnulALT2  35712  linedegen  36908  nexntru  37192  nexfal  37193  unqsym1  37213  elttcirr  37319  bj-dtrucor2v  37729  bj-ru1  37856  bj-0nelsngl  37884  bj-ccinftydisj  38135  disjALTV0  39787  dtrucor3  49909