Metamath Proof Explorer

Theorem difss2

Description: If a class is contained in a difference, it is contained in the minuend. (Contributed by David Moews, 1-May-2017)

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

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A C_ ( B \ C ) -> A C_ ( B \ C ) )
2 difss 
 |-  ( B \ C ) C_ B
3 1 2 sstrdi 
 |-  ( A C_ ( B \ C ) -> A C_ B )