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	$$⊢\phi \to A\subseteq B$$
Assertion	ssdifssd	$$⊢\phi \to A\setminus C\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		ssdifd.1	$$⊢\phi \to A\subseteq B$$
2		ssdifss	$$⊢A\subseteq B\to A\setminus C\subseteq B$$
3	1 2	syl	$$⊢\phi \to A\setminus C\subseteq B$$