Metamath Proof Explorer


Theorem ssdifssd

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

Ref Expression
Hypothesis ssdifd.1 ( 𝜑𝐴𝐵 )
Assertion ssdifssd ( 𝜑 → ( 𝐴𝐶 ) ⊆ 𝐵 )

Proof

Step Hyp Ref Expression
1 ssdifd.1 ( 𝜑𝐴𝐵 )
2 ssdifss ( 𝐴𝐵 → ( 𝐴𝐶 ) ⊆ 𝐵 )
3 1 2 syl ( 𝜑 → ( 𝐴𝐶 ) ⊆ 𝐵 )