Theorem sseq0

Description: A subclass of an empty class is empty. (Contributed by NM, 7-Mar-2007) (Proof shortened by Andrew Salmon, 26-Jun-2011)

	Ref	Expression
Assertion	sseq0	$$⊢\left(A\subseteq B\wedge B=\varnothing \right)\to A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		sseq2	$$⊢B=\varnothing \to \left(A\subseteq B\leftrightarrow A\subseteq \varnothing \right)$$
2		ss0	$$⊢A\subseteq \varnothing \to A=\varnothing$$
3	1 2	biimtrdi	$$⊢B=\varnothing \to \left(A\subseteq B\to A=\varnothing \right)$$
4	3	impcom	$$⊢\left(A\subseteq B\wedge B=\varnothing \right)\to A=\varnothing$$