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 209  df-ex 1781

This theorem is referenced by:  ru  3771  noel  4296  axnulALT  5208  notzfaus  5262  notzfausOLD  5263  dtrucor2  5273  opelopabsb  5417  0nelxp  5589  0xp  5649  dm0  5790  cnv0  5999  co02  6113  dffv3  6666  mpo0  7239  canth2  8670  brdom3  9950  ruc  15596  meet0  17747  join0  17748  0g0  17874  ustn0  22829  bnj1523  32343  linedegen  33604  nexntru  33752  nexfal  33753  unqsym1  33773  amosym1  33774  subsym1  33775  bj-dtrucor2v  34140  bj-ru1  34257  bj-0nelsngl  34286  bj-ccinftydisj  34498  disjALTV0  35999  nsb  39121