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  3739  ruOLD  3740  noel  4288  axnulALT  5242  notzfaus  5301  dtrucor2  5310  opelopabsb  5470  0nelopab  5505  0nelxp  5650  0xp  5715  dm0  5860  cnv0  6087  co02  6208  dffv3  6818  mpo0  7431  canth2  9043  snnen2o  9129  1sdom2dom  9138  brdom3  10419  ruc  16152  join0  18309  meet0  18310  0g0  18572  ustn0  24137  bnj1523  35081  linedegen  36183  nexntru  36444  nexfal  36445  unqsym1  36465  bj-dtrucor2v  36857  bj-ru1  36983  bj-0nelsngl  37011  bj-ccinftydisj  37253  disjALTV0  38798  dtrucor3  48836