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	⊢ ¬ 𝐴 ⊊ ∅

Proof

Step	Hyp	Ref	Expression
1		0ss	⊢ ∅ ⊆ 𝐴
2		ssnpss	⊢ ( ∅ ⊆ 𝐴 → ¬ 𝐴 ⊊ ∅ )
3	1 2	ax-mp	⊢ ¬ 𝐴 ⊊ ∅