pssdifcom1

Description: Two ways to express overlapping subsets. (Contributed by Stefan O'Rear, 31-Oct-2014)

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

Step	Hyp	Ref	Expression
1		difcom	$⊢ C ∖ A \subseteq B \leftrightarrow C ∖ B \subseteq A$
2	1	a1i	$⊢ (A \subseteq C \land B \subseteq C) \to (C ∖ A \subseteq B \leftrightarrow C ∖ B \subseteq A)$
3		ssconb	$⊢ (B \subseteq C \land A \subseteq C) \to (B \subseteq C ∖ A \leftrightarrow A \subseteq C ∖ B)$
4	3	ancoms	$⊢ (A \subseteq C \land B \subseteq C) \to (B \subseteq C ∖ A \leftrightarrow A \subseteq C ∖ B)$
5	4	notbid	$⊢ (A \subseteq C \land B \subseteq C) \to (\neg B \subseteq C ∖ A \leftrightarrow \neg A \subseteq C ∖ B)$
6	2 5	anbi12d	$⊢ (A \subseteq C \land B \subseteq C) \to ((C ∖ A \subseteq B \land \neg B \subseteq C ∖ A) \leftrightarrow (C ∖ B \subseteq A \land \neg A \subseteq C ∖ B))$
7		dfpss3	$⊢ C ∖ A \subset B \leftrightarrow (C ∖ A \subseteq B \land \neg B \subseteq C ∖ A)$
8		dfpss3	$⊢ C ∖ B \subset A \leftrightarrow (C ∖ B \subseteq A \land \neg A \subseteq C ∖ B)$
9	6 7 8	3bitr4g	$⊢ (A \subseteq C \land B \subseteq C) \to (C ∖ A \subset B \leftrightarrow C ∖ B \subset A)$

Metamath Proof Explorer