pssdifcom2

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

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

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

Metamath Proof Explorer