Metamath Proof Explorer


Theorem ssdifss

Description: Preservation of a subclass relationship by class difference. (Contributed by NM, 15-Feb-2007)

Ref Expression
Assertion ssdifss ( 𝐴𝐵 → ( 𝐴𝐶 ) ⊆ 𝐵 )

Proof

Step Hyp Ref Expression
1 difss ( 𝐴𝐶 ) ⊆ 𝐴
2 sstr ( ( ( 𝐴𝐶 ) ⊆ 𝐴𝐴𝐵 ) → ( 𝐴𝐶 ) ⊆ 𝐵 )
3 1 2 mpan ( 𝐴𝐵 → ( 𝐴𝐶 ) ⊆ 𝐵 )