This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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