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

Metamath Proof Explorer

Theorem ssdif

Description: Difference law for subsets. (Contributed by NM, 28-May-1998)

		Ref	Expression
	Assertion	ssdif	$⊢ A \subseteq B \to A ∖ C \subseteq B ∖ C$

Step	Hyp	Ref	Expression
1		ssel	$⊢ A \subseteq B \to (x \in A \to x \in B)$
2	1	anim1d	$⊢ A \subseteq B \to ((x \in A \land \neg x \in C) \to (x \in B \land \neg x \in C))$
3		eldif	$⊢ x \in (A ∖ C) \leftrightarrow (x \in A \land \neg x \in C)$
4		eldif	$⊢ x \in (B ∖ C) \leftrightarrow (x \in B \land \neg x \in C)$
5	2 3 4	3imtr4g	$⊢ A \subseteq B \to (x \in (A ∖ C) \to x \in (B ∖ C))$
6	5	ssrdv	$⊢ A \subseteq B \to A ∖ C \subseteq B ∖ C$