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  3763  ruOLD  3764  noel  4313  axnulALT  5274  notzfaus  5333  dtrucor2  5342  opelopabsb  5505  0nelopab  5542  0nelxp  5688  0xp  5753  dm0  5900  cnv0  6129  co02  6249  dffv3  6871  mpo0  7490  canth2  9142  snnen2o  9243  1sdom2dom  9253  brdom3  10540  ruc  16259  join0  18413  meet0  18414  0g0  18640  ustn0  24157  bnj1523  35048  linedegen  36107  nexntru  36368  nexfal  36369  unqsym1  36389  bj-dtrucor2v  36781  bj-ru1  36907  bj-0nelsngl  36935  bj-ccinftydisj  37177  disjALTV0  38718  dtrucor3  48726