Theorem nex 1801

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

Syntax hints:  ¬ wn 3  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796

This theorem depends on definitions:  df-bi 207  df-ex 1781

This theorem is referenced by:  ru  3735  ruOLD  3736  noel  4287  uni0  4888  axnulALT  5246  notzfaus  5305  dtrucor2  5314  opelopabsb  5475  0nelopab  5510  0nelxp  5655  0xp  5720  xp0  5721  dm0  5866  cnv0  6094  cnv0OLD  6095  co02  6216  dffv3  6827  mpo0  7440  canth2  9054  snnen2o  9140  1sdom2dom  9149  brdom3  10430  ruc  16159  join0  18317  meet0  18318  0g0  18580  ustn0  24156  bnj1523  35155  linedegen  36259  nexntru  36520  nexfal  36521  unqsym1  36541  bj-dtrucor2v  36934  bj-ru1  37060  bj-0nelsngl  37088  bj-ccinftydisj  37330  disjALTV0  38925  dtrucor3  48960