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  3751  ruOLD  3752  noel  4301  axnulALT  5259  notzfaus  5318  dtrucor2  5327  opelopabsb  5490  0nelopab  5527  0nelxp  5672  0xp  5737  dm0  5884  cnv0  6113  co02  6233  dffv3  6854  mpo0  7474  canth2  9094  snnen2o  9184  1sdom2dom  9194  brdom3  10481  ruc  16211  join0  18364  meet0  18365  0g0  18591  ustn0  24108  bnj1523  35061  linedegen  36131  nexntru  36392  nexfal  36393  unqsym1  36413  bj-dtrucor2v  36805  bj-ru1  36931  bj-0nelsngl  36959  bj-ccinftydisj  37201  disjALTV0  38746  dtrucor3  48787