Theorem ssdif2d

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

	Ref	Expression
Hypotheses	ssdifd.1	$$⊢\phi \to A\subseteq B$$
	ssdif2d.2	$$⊢\phi \to C\subseteq D$$
Assertion	ssdif2d	$$⊢\phi \to A\setminus D\subseteq B\setminus C$$

Proof

Step	Hyp	Ref	Expression
1		ssdifd.1	$$⊢\phi \to A\subseteq B$$
2		ssdif2d.2	$$⊢\phi \to C\subseteq D$$
3	2	sscond	$$⊢\phi \to A\setminus D\subseteq A\setminus C$$
4	1	ssdifd	$$⊢\phi \to A\setminus C\subseteq B\setminus C$$
5	3 4	sstrd	$$⊢\phi \to A\setminus D\subseteq B\setminus C$$