Theorem nex 1808

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

Syntax hints:  ¬ wn 3  ∃wex 1787

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

This theorem depends on definitions:  df-bi 210  df-ex 1788

This theorem is referenced by:  ru  3682  noel  4231  noelOLD  4232  axnulALT  5182  notzfaus  5239  notzfausOLD  5240  dtrucor2  5250  opelopabsb  5396  0nelopab  5431  0nelxp  5570  0xp  5631  dm0  5774  cnv0  5984  co02  6104  dffv3  6691  mpo0  7274  canth2  8777  brdom3  10107  ruc  15767  join0  17865  meet0  17866  0g0  18090  ustn0  23072  bnj1523  32718  linedegen  34131  nexntru  34279  nexfal  34280  unqsym1  34300  amosym1  34301  subsym1  34302  bj-dtrucor2v  34686  bj-ru1  34818  bj-0nelsngl  34847  bj-ccinftydisj  35068  disjALTV0  36548  dtrucor3  45760