Theorem ssdifd

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

	Ref	Expression
Hypothesis	ssdifd.1	$$⊢\phi \to A\subseteq B$$
Assertion	ssdifd	$$⊢\phi \to A\setminus C\subseteq B\setminus C$$

Proof

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