Theorem nex 1880

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

Syntax hints:  ¬ wn 3  ∃wex 1853

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

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

This theorem is referenced by:  ru  3575  axnulALT  4939  notzfaus  4989  dtrucor2  5050  opelopabsb  5135  0nelxp  5300  0nelxpOLD  5301  0xp  5356  dm0  5494  cnv0  5693  co02  5810  dffv3  6348  mpt20  6890  canth2  8278  brdom3  9542  ruc  15171  meet0  17338  join0  17339  0g0  17464  ustn0  22225  bnj1523  31446  linedegen  32556  nextnt  32710  nextf  32711  unqsym1  32730  amosym1  32731  subsym1  32732  bj-dtrucor2v  33107  bj-ru1  33239  bj-0nelsngl  33265  bj-ccinftydisj  33411