Theorem nalfal

Description: Not all sets hold F. as true. (Contributed by Anthony Hart, 13-Sep-2011)

	Ref	Expression
Assertion	nalfal	$$⊢\neg \forall x\perp$$

Proof

Step	Hyp	Ref	Expression
1		alfal	$$⊢\forall x\neg \perp$$
2		falim	$$⊢\perp \to \neg \forall x\neg \perp$$
3	2	sps	$$⊢\forall x\perp \to \neg \forall x\neg \perp$$
4	1 3	mt2	$$⊢\neg \forall x\perp$$