Theorem nex 1879

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

Syntax hints:  ¬ wn 3  ∃wex 1852

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

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

This theorem is referenced by:  ru  3586  axnulALT  4921  notzfaus  4971  dtrucor2  5029  opelopabsb  5118  0nelxp  5283  0nelxpOLD  5284  0xp  5339  dm0  5477  cnv0  5676  co02  5793  dffv3  6328  mpt20  6872  canth2  8269  brdom3  9552  ruc  15178  meet0  17345  join0  17346  0g0  17471  ustn0  22244  bnj1523  31477  linedegen  32587  nextnt  32741  nextf  32742  unqsym1  32761  amosym1  32762  subsym1  32763  bj-dtrucor2v  33137  bj-ru1  33265  bj-0nelsngl  33290  bj-ccinftydisj  33437