sscon

Description: Contraposition law for subsets. Exercise 15 of TakeutiZaring p. 22. (Contributed by NM, 22-Mar-1998)

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

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

Metamath Proof Explorer