Metamath Proof Explorer

Theorem difss2d

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

Ref Expression
Hypothesis difss2d.1 φ A B C
Assertion difss2d φ A B


Step Hyp Ref Expression
1 difss2d.1 φ A B C
2 difss2 A B C A B
3 1 2 syl φ A B