Metamath Proof Explorer

Theorem ssdifss

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

Ref Expression
Assertion ssdifss 
|- ( A C_ B -> ( A \ C ) C_ B )

Proof

Step Hyp Ref Expression
1 difss 
 |-  ( A \ C ) C_ A
2 sstr 
 |-  ( ( ( A \ C ) C_ A /\ A C_ B ) -> ( A \ C ) C_ B )
3 1 2 mpan 
 |-  ( A C_ B -> ( A \ C ) C_ B )