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

Proof

Step	Hyp	Ref	Expression
1		sseq0b	⊢ ( 𝐵 = ∅ → ( 𝐴 ⊆ 𝐵 ↔ 𝐴 = ∅ ) )
2	1	biimpac	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅ ) → 𝐴 = ∅ )