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 206  df-ex 1782

This theorem is referenced by:  ru  3741  noel  4295  noelOLD  4296  axnulALT  5266  notzfaus  5323  dtrucor2  5332  opelopabsb  5492  0nelopab  5529  0nelxp  5672  0xp  5735  dm0  5881  cnv0  6098  co02  6217  dffv3  6843  mpo0  7447  canth2  9081  snnen2o  9188  1sdom2dom  9198  brdom3  10473  ruc  16136  join0  18308  meet0  18309  0g0  18533  ustn0  23609  bnj1523  33772  linedegen  34804  nexntru  34952  nexfal  34953  unqsym1  34973  bj-dtrucor2v  35358  bj-ru1  35487  bj-0nelsngl  35515  bj-ccinftydisj  35757  disjALTV0  37289  dtrucor3  47004