Theorem sseq0b

Description: The only subclass of the empty class is itself. (Contributed by NM, 7-Mar-2007) (Proof shortened by Andrew Salmon, 26-Jun-2011) Strengthen sseq0 to a biconditional. (Revised by BJ, 19-Jul-2026)

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

Proof

Step	Hyp	Ref	Expression
1		sseq2	$$⊢A=\varnothing \to \left(B\subseteq A\leftrightarrow B\subseteq \varnothing \right)$$
2		ss0b	$$⊢B\subseteq \varnothing \leftrightarrow B=\varnothing$$
3	1 2	bitrdi	$$⊢A=\varnothing \to \left(B\subseteq A\leftrightarrow B=\varnothing \right)$$