Theorem nex 1801

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

Syntax hints:  ¬ wn 3  ∃wex 1780

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

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

This theorem is referenced by:  ru  3738  ruOLD  3739  noel  4290  uni0  4891  axnulALT  5249  notzfaus  5308  dtrucor2  5317  opelopabsb  5478  0nelopab  5513  0nelxp  5658  0xp  5723  xp0  5724  dm0  5869  cnv0  6097  cnv0OLD  6098  co02  6219  dffv3  6830  mpo0  7443  canth2  9058  snnen2o  9145  1sdom2dom  9154  brdom3  10438  ruc  16168  join0  18326  meet0  18327  0g0  18589  ustn0  24165  bnj1523  35227  linedegen  36337  nexntru  36598  nexfal  36599  unqsym1  36619  bj-dtrucor2v  37018  bj-ru1  37144  bj-0nelsngl  37172  bj-ccinftydisj  37418  disjALTV0  39013  dtrucor3  49044