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  3754  ruOLD  3755  noel  4304  axnulALT  5262  notzfaus  5321  dtrucor2  5330  opelopabsb  5493  0nelopab  5530  0nelxp  5675  0xp  5740  dm0  5887  cnv0  6116  co02  6236  dffv3  6857  mpo0  7477  canth2  9100  snnen2o  9191  1sdom2dom  9201  brdom3  10488  ruc  16218  join0  18371  meet0  18372  0g0  18598  ustn0  24115  bnj1523  35068  linedegen  36138  nexntru  36399  nexfal  36400  unqsym1  36420  bj-dtrucor2v  36812  bj-ru1  36938  bj-0nelsngl  36966  bj-ccinftydisj  37208  disjALTV0  38753  dtrucor3  48791