Theorem nex 1833

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

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

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

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

This theorem is used by:  ru  3745  noel  4291  uni0  4903  axnulALT  5269  vnex  5282  notsep  5336  dtrucor2  5345  opelopabsb  5516  0nelopab  5552  0nelxp  5697  0xp  5762  xp0  5763  cnv0  5871  cnv0OLD  5872  dm0  5912  co02  6264  dffv3  6881  mpo0  7501  canth2  9121  snnen2o  9208  1sdom2dom  9217  brdom3  10523  ruc  16316  join0  18476  meet0  18477  0g0  18739  ustn0  24407  bnj1523  35483  axnulALT2  35493  linedegen  36648  nexntru  36948  nexfal  36949  unqsym1  36969  elttcirr  37075  bj-dtrucor2v  37485  bj-ru1  37612  bj-0nelsngl  37640  bj-ccinftydisj  37890  disjALTV0  39536  dtrucor3  49610