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  3742  ruOLD  3743  noel  4291  axnulALT  5246  notzfaus  5305  dtrucor2  5314  opelopabsb  5477  0nelopab  5512  0nelxp  5657  0xp  5722  dm0  5867  cnv0  6093  co02  6213  dffv3  6822  mpo0  7438  canth2  9054  snnen2o  9144  1sdom2dom  9153  brdom3  10441  ruc  16170  join0  18327  meet0  18328  0g0  18556  ustn0  24124  bnj1523  35040  linedegen  36119  nexntru  36380  nexfal  36381  unqsym1  36401  bj-dtrucor2v  36793  bj-ru1  36919  bj-0nelsngl  36947  bj-ccinftydisj  37189  disjALTV0  38734  dtrucor3  48787