sscon34b

Description: Relative complementation reverses inclusion of subclasses. Relativized version of complss . (Contributed by RP, 3-Jun-2021)

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

Step	Hyp	Ref	Expression
1		sscon	$⊢ A \subseteq B \to C ∖ B \subseteq C ∖ A$
2		sscon	$⊢ C ∖ B \subseteq C ∖ A \to C ∖ (C ∖ A) \subseteq C ∖ (C ∖ B)$
3		dfss4	$⊢ A \subseteq C \leftrightarrow C ∖ (C ∖ A) = A$
4	3	birani	$⊢ (A \subseteq C \land B \subseteq C) \to C ∖ (C ∖ A) = A$
5		dfss4	$⊢ B \subseteq C \leftrightarrow C ∖ (C ∖ B) = B$
6	5	bilani	$⊢ (A \subseteq C \land B \subseteq C) \to C ∖ (C ∖ B) = B$
7	4 6	sseq12d	$⊢ (A \subseteq C \land B \subseteq C) \to (C ∖ (C ∖ A) \subseteq C ∖ (C ∖ B) \leftrightarrow A \subseteq B)$
8	2 7	imbitrid	$⊢ (A \subseteq C \land B \subseteq C) \to (C ∖ B \subseteq C ∖ A \to A \subseteq B)$
9	1 8	impbid2	$⊢ (A \subseteq C \land B \subseteq C) \to (A \subseteq B \leftrightarrow C ∖ B \subseteq C ∖ A)$

Metamath Proof Explorer