Theorem 0pss

Description: The empty set is a proper subset of any nonempty set. Dual of pssv . (Contributed by NM, 27-Feb-1996)

	Ref	Expression
Assertion	0pss	$$⊢\varnothing \subset A\leftrightarrow A\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		0ss	$$⊢\varnothing \subseteq A$$
2		df-pss	$$⊢\varnothing \subset A\leftrightarrow \left(\varnothing \subseteq A\wedge \varnothing \ne A\right)$$
3	1 2	mpbiran	$$⊢\varnothing \subset A\leftrightarrow \varnothing \ne A$$
4		necom	$$⊢\varnothing \ne A\leftrightarrow A\ne \varnothing$$
5	3 4	bitri	$$⊢\varnothing \subset A\leftrightarrow A\ne \varnothing$$