Theorem ss0b

Description: Any subset of the empty set is empty. Theorem 5 of Suppes p. 23 and its converse. (Contributed by NM, 17-Sep-2003)

	Ref	Expression
Assertion	ss0b	$$⊢A\subseteq \varnothing \leftrightarrow A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		0ss	$$⊢\varnothing \subseteq A$$
2		eqss	$$⊢A=\varnothing \leftrightarrow \left(A\subseteq \varnothing \wedge \varnothing \subseteq A\right)$$
3	1 2	mpbiran2	$$⊢A=\varnothing \leftrightarrow A\subseteq \varnothing$$
4	3	bicomi	$$⊢A\subseteq \varnothing \leftrightarrow A=\varnothing$$