Theorem nex 1832

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

This proof depends on syntax axioms:  ¬ wn 3  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827

This proof depends on definitions:  df-bi 210  df-ex 1812

This theorem is used by:  ru  3737  noel  4282  noelOLD  4283  uni0  4895  axnulALT  5257  vnex  5270  notsep  5325  dtrucor2  5334  opelopabsb  5504  0nelopab  5540  0nelxp  5685  0xp  5751  xp0  5752  cnv0  5862  cnv0OLD  5863  dm0  5903  co02  6265  dffv3  6886  mpo0  7509  canth2  9156  snnen2o  9243  1sdom2dom  9252  brdom3  10614  ruc  16420  join0  18586  meet0  18587  0g0  18853  ustn0  24549  bnj1523  35751  axnulALT2  35764  onf1oracwevd  35975  linedegen  37004  nexntru  37288  nexfal  37289  unqsym1  37309  elttcirr  37415  bj-dtrucor2v  37825  bj-ru1  37952  bj-0nelsngl  37980  bj-ccinftydisj  38243  disjALTV0  39895  dtrucor3  50017