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	⊢ ( 𝐴 = ∅ → ( 𝐵 ⊆ 𝐴 ↔ 𝐵 = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		sseq2	⊢ ( 𝐴 = ∅ → ( 𝐵 ⊆ 𝐴 ↔ 𝐵 ⊆ ∅ ) )
2		ss0b	⊢ ( 𝐵 ⊆ ∅ ↔ 𝐵 = ∅ )
3	1 2	bitrdi	⊢ ( 𝐴 = ∅ → ( 𝐵 ⊆ 𝐴 ↔ 𝐵 = ∅ ) )