Theorem nex 1731

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

Syntax hints:  ¬ wn 3  ∃wex 1704

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

This theorem depends on definitions:  df-bi 197  df-ex 1705

This theorem is referenced by:  ru  3434  axnulALT  4787  notzfaus  4840  dtrucor2  4901  opelopabsb  4985  0nelxp  5143  0nelxpOLD  5144  0xp  5199  dm0  5339  cnv0  5535  co02  5649  dffv3  6187  mpt20  6725  canth2  8113  brdom3  9350  ruc  14972  meet0  17137  join0  17138  0g0  17263  ustn0  22024  bnj1523  31139  linedegen  32250  nextnt  32404  nextf  32405  unqsym1  32424  amosym1  32425  subsym1  32426  bj-dtrucor2v  32801  bj-ru1  32933  bj-0nelsngl  32959  bj-ccinftydisj  33100