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 ABCAB

Proof

Step Hyp Ref Expression
1 id ABCABC
2 difss BCB
3 1 2 sstrdi ABCAB