Theorem gennall-P6 730

Description: The WFF '¬ ∀𝑥𝜑' is General For '𝑥'.

If this result is stated as an axiom (ax-L10 27), then all the other related "general for" rules will follow (though half will require ax-L12 29 as well).

See gennallw-P6 678 for a version that requires only FOL axioms.

Assertion

Ref	Expression
gennall-P6	⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)

Proof of Theorem gennall-P6

Step	Hyp	Ref	Expression
1		ax-L10 27	1 ⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)

Syntax hints:  ∀wff-forall 8  ¬ wff-neg 9   → wff-imp 10

This theorem was proved from axioms:  ax-L10 27

This theorem is referenced by:  genex-P6  731  exgenall-P6  732  genall-P6  737