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

Metamath Proof Explorer

Theorem ssconb

Description: Contraposition law for subsets. (Contributed by NM, 22-Mar-1998)

		Ref	Expression
	Assertion	ssconb	$⊢ (A \subseteq C \land B \subseteq C) \to (A \subseteq C ∖ B \leftrightarrow B \subseteq C ∖ A)$

Proof

Step	Hyp	Ref	Expression
1		ssel	$⊢ A \subseteq C \to (x \in A \to x \in C)$
2		ssel	$⊢ B \subseteq C \to (x \in B \to x \in C)$
3		pm5.1	$⊢ ((x \in A \to x \in C) \land (x \in B \to x \in C)) \to ((x \in A \to x \in C) \leftrightarrow (x \in B \to x \in C))$
4	1 2 3	syl2an	$⊢ (A \subseteq C \land B \subseteq C) \to ((x \in A \to x \in C) \leftrightarrow (x \in B \to x \in C))$
5		con2b	$⊢ (x \in A \to \neg x \in B) \leftrightarrow (x \in B \to \neg x \in A)$
6	5	a1i	$⊢ (A \subseteq C \land B \subseteq C) \to ((x \in A \to \neg x \in B) \leftrightarrow (x \in B \to \neg x \in A))$
7	4 6	anbi12d	$⊢ (A \subseteq C \land B \subseteq C) \to (((x \in A \to x \in C) \land (x \in A \to \neg x \in B)) \leftrightarrow ((x \in B \to x \in C) \land (x \in B \to \neg x \in A)))$
8		jcab	$⊢ (x \in A \to (x \in C \land \neg x \in B)) \leftrightarrow ((x \in A \to x \in C) \land (x \in A \to \neg x \in B))$
9		jcab	$⊢ (x \in B \to (x \in C \land \neg x \in A)) \leftrightarrow ((x \in B \to x \in C) \land (x \in B \to \neg x \in A))$
10	7 8 9	3bitr4g	$⊢ (A \subseteq C \land B \subseteq C) \to ((x \in A \to (x \in C \land \neg x \in B)) \leftrightarrow (x \in B \to (x \in C \land \neg x \in A)))$
11		eldif	$⊢ x \in (C ∖ B) \leftrightarrow (x \in C \land \neg x \in B)$
12	11	imbi2i	$⊢ (x \in A \to x \in (C ∖ B)) \leftrightarrow (x \in A \to (x \in C \land \neg x \in B))$
13		eldif	$⊢ x \in (C ∖ A) \leftrightarrow (x \in C \land \neg x \in A)$
14	13	imbi2i	$⊢ (x \in B \to x \in (C ∖ A)) \leftrightarrow (x \in B \to (x \in C \land \neg x \in A))$
15	10 12 14	3bitr4g	$⊢ (A \subseteq C \land B \subseteq C) \to ((x \in A \to x \in (C ∖ B)) \leftrightarrow (x \in B \to x \in (C ∖ A)))$
16	15	albidv	$⊢ (A \subseteq C \land B \subseteq C) \to (\forall x (x \in A \to x \in (C ∖ B)) \leftrightarrow \forall x (x \in B \to x \in (C ∖ A)))$
17		df-ss	$⊢ A \subseteq C ∖ B \leftrightarrow \forall x (x \in A \to x \in (C ∖ B))$
18		df-ss	$⊢ B \subseteq C ∖ A \leftrightarrow \forall x (x \in B \to x \in (C ∖ A))$
19	16 17 18	3bitr4g	$⊢ (A \subseteq C \land B \subseteq C) \to (A \subseteq C ∖ B \leftrightarrow B \subseteq C ∖ A)$