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		sseq0b	$$⊢B=\varnothing \to \left(A\subseteq B\leftrightarrow A=\varnothing \right)$$
2	1	biimpac	$$⊢\left(A\subseteq B\wedge B=\varnothing \right)\to A=\varnothing$$