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  3740  ruOLD  3741  noel  4292  uni0  4893  axnulALT  5251  notzfaus  5310  dtrucor2  5319  opelopabsb  5486  0nelopab  5521  0nelxp  5666  0xp  5731  xp0  5732  dm0  5877  cnv0  6105  cnv0OLD  6106  co02  6227  dffv3  6838  mpo0  7453  canth2  9070  snnen2o  9157  1sdom2dom  9166  brdom3  10450  ruc  16180  join0  18338  meet0  18339  0g0  18601  ustn0  24177  bnj1523  35246  linedegen  36356  nexntru  36617  nexfal  36618  unqsym1  36638  bj-dtrucor2v  37062  bj-ru1  37188  bj-0nelsngl  37216  bj-ccinftydisj  37465  disjALTV0  39102  dtrucor3  49155