Metamath Proof Explorer

Theorem difssd

Description: A difference of two classes is contained in the minuend. Deduction form of difss . (Contributed by David Moews, 1-May-2017)

Ref Expression
Assertion difssd 
|- ( ph -> ( A \ B ) C_ A )

Proof

Step Hyp Ref Expression
1 difss 
 |-  ( A \ B ) C_ A
2 1 a1i 
 |-  ( ph -> ( A \ B ) C_ A )