This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∖ C \subseteq B$

Step	Hyp	Ref	Expression
1		difss	$⊢ A ∖ C \subseteq A$
2		sstr	$⊢ (A ∖ C \subseteq A \land A \subseteq B) \to A ∖ C \subseteq B$
3	1 2	mpan	$⊢ A \subseteq B \to A ∖ C \subseteq B$