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		sseq2	⊢ ( 𝐵 = ∅ → ( 𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ ∅ ) )
2		ss0	⊢ ( 𝐴 ⊆ ∅ → 𝐴 = ∅ )
3	1 2	biimtrdi	⊢ ( 𝐵 = ∅ → ( 𝐴 ⊆ 𝐵 → 𝐴 = ∅ ) )
4	3	impcom	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅ ) → 𝐴 = ∅ )