Metamath Proof Explorer


Theorem sscond

Description: If A is contained in B , then ( C \ B ) is contained in ( C \ A ) . Deduction form of sscon . (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypothesis ssdifd.1 φAB
Assertion sscond φCBCA

Proof

Step Hyp Ref Expression
1 ssdifd.1 φAB
2 sscon ABCBCA
3 1 2 syl φCBCA