Theorem nex 779

Description: Generalization rule for negated wff.

Hypothesis

Ref	Expression
nex.1	⊢ ¬ φ

Assertion

Ref	Expression
nex	⊢ ¬ ∃xφ

Proof of Theorem nex

Step	Hyp	Ref	Expression
1		alnex 716	. 2 ⊢ (∀x ¬ φ ↔ ¬ ∃xφ)
2		nex.1	. 2 ⊢ ¬ φ
3	1, 2	mpgbi 685	1 ⊢ ¬ ∃xφ

Syntax hints:  ¬ wn 1  ∃wex 678

This theorem is referenced by:  ru 1437  rab0 1718  xp0r 2474  0nelxp 2475  dm0 2542  dmsn0 2543  dmsnsn0 2544  co02 2663  0nelqs 3234  canth2 3381  cfsuc 3709  nnunb 4520  ruc 4924

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-gen 677

This theorem depends on definitions:  df-bi 128  df-ex 679

metamath.org