Description: If a class is contained in a difference, it is contained in the minuend. Deduction form of difss2 . (Contributed by David Moews, 1May2017)
Ref  Expression  

Hypothesis  difss2d.1   ( ph > A C_ ( B \ C ) ) 

Assertion  difss2d   ( ph > A C_ B ) 
Step  Hyp  Ref  Expression 

1  difss2d.1   ( ph > A C_ ( B \ C ) ) 

2  difss2   ( A C_ ( B \ C ) > A C_ B ) 

3  1 2  syl   ( ph > A C_ B ) 