Theorem ssdifss

Description: Preservation of a subclass relationship by class difference. (Contributed by NM, 15-Feb-2007)

	Ref	Expression
Assertion	ssdifss	$$⊢A\subseteq B\to A\setminus C\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		difss	$$⊢A\setminus C\subseteq A$$
2		sstr	$$⊢\left(A\setminus C\subseteq A\wedge A\subseteq B\right)\to A\setminus C\subseteq B$$
3	1 2	mpan	$$⊢A\subseteq B\to A\setminus C\subseteq B$$