Theorem nex 1802

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

Syntax hints:  ¬ wn 3  ∃wex 1781

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

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

This theorem is referenced by:  ru  3727  ruOLD  3728  noel  4279  uni0  4879  axnulALT  5239  notzfaus  5300  dtrucor2  5309  opelopabsb  5478  0nelopab  5513  0nelxp  5658  0xp  5723  xp0  5724  dm0  5869  cnv0  6097  cnv0OLD  6098  co02  6219  dffv3  6830  mpo0  7445  canth2  9061  snnen2o  9148  1sdom2dom  9157  brdom3  10441  ruc  16201  join0  18360  meet0  18361  0g0  18623  ustn0  24196  bnj1523  35229  axnulALT2  35240  linedegen  36341  nexntru  36602  nexfal  36603  unqsym1  36623  elttcirr  36729  bj-dtrucor2v  37140  bj-ru1  37266  bj-0nelsngl  37294  bj-ccinftydisj  37543  disjALTV0  39189  dtrucor3  49286