Theorem npss0

Description: No set is a proper subset of the empty set. (Contributed by NM, 17-Jun-1998) (Proof shortened by Andrew Salmon, 26-Jun-2011) (Proof shortened by JJ, 14-Jul-2021)

	Ref	Expression
Assertion	npss0	$$⊢\neg A\subset \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		0ss	$$⊢\varnothing \subseteq A$$
2		ssnpss	$$⊢\varnothing \subseteq A\to \neg A\subset \varnothing$$
3	1 2	ax-mp	$$⊢\neg A\subset \varnothing$$