Metamath Proof Explorer


Theorem ssin0

Description: If two classes are disjoint, two respective subclasses are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion ssin0 ( ( ( 𝐴𝐵 ) = ∅ ∧ 𝐶𝐴𝐷𝐵 ) → ( 𝐶𝐷 ) = ∅ )

Proof

Step Hyp Ref Expression
1 ss2in ( ( 𝐶𝐴𝐷𝐵 ) → ( 𝐶𝐷 ) ⊆ ( 𝐴𝐵 ) )
2 1 3adant1 ( ( ( 𝐴𝐵 ) = ∅ ∧ 𝐶𝐴𝐷𝐵 ) → ( 𝐶𝐷 ) ⊆ ( 𝐴𝐵 ) )
3 eqimss ( ( 𝐴𝐵 ) = ∅ → ( 𝐴𝐵 ) ⊆ ∅ )
4 3 3ad2ant1 ( ( ( 𝐴𝐵 ) = ∅ ∧ 𝐶𝐴𝐷𝐵 ) → ( 𝐴𝐵 ) ⊆ ∅ )
5 2 4 sstrd ( ( ( 𝐴𝐵 ) = ∅ ∧ 𝐶𝐴𝐷𝐵 ) → ( 𝐶𝐷 ) ⊆ ∅ )
6 ss0 ( ( 𝐶𝐷 ) ⊆ ∅ → ( 𝐶𝐷 ) = ∅ )
7 5 6 syl ( ( ( 𝐴𝐵 ) = ∅ ∧ 𝐶𝐴𝐷𝐵 ) → ( 𝐶𝐷 ) = ∅ )