Theorem nex 1800

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

Syntax hints:  ¬ wn 3  ∃wex 1779

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

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

This theorem is referenced by:  ru  3786  ruOLD  3787  noel  4338  axnulALT  5304  notzfaus  5363  dtrucor2  5372  opelopabsb  5535  0nelopab  5572  0nelxp  5719  0xp  5784  dm0  5931  cnv0  6160  co02  6280  dffv3  6902  mpo0  7518  canth2  9170  snnen2o  9273  1sdom2dom  9283  brdom3  10568  ruc  16279  join0  18450  meet0  18451  0g0  18677  ustn0  24229  bnj1523  35085  linedegen  36144  nexntru  36405  nexfal  36406  unqsym1  36426  bj-dtrucor2v  36818  bj-ru1  36944  bj-0nelsngl  36972  bj-ccinftydisj  37214  disjALTV0  38755  dtrucor3  48719