Metamath Proof Explorer

Theorem reldisjOLD

Description: Obsolete version of reldisj as of 28-Jun-2024. (Contributed by NM, 15-Feb-2007) (Proof shortened by Andrew Salmon, 26-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	reldisjOLD	$⊢ A \subseteq C \to (A \cap B = \emptyset \leftrightarrow A \subseteq C ∖ B)$

Proof

Step	Hyp	Ref	Expression
1		dfss2	$⊢ A \subseteq C \leftrightarrow \forall x (x \in A \to x \in C)$
2		pm5.44	$⊢ (x \in A \to x \in C) \to ((x \in A \to \neg x \in B) \leftrightarrow (x \in A \to (x \in C \land \neg x \in B)))$
3		eldif	$⊢ x \in (C ∖ B) \leftrightarrow (x \in C \land \neg x \in B)$
4	3	imbi2i	$⊢ (x \in A \to x \in (C ∖ B)) \leftrightarrow (x \in A \to (x \in C \land \neg x \in B))$
5	2 4	bitr4di	$⊢ (x \in A \to x \in C) \to ((x \in A \to \neg x \in B) \leftrightarrow (x \in A \to x \in (C ∖ B)))$
6	5	sps	$⊢ \forall x (x \in A \to x \in C) \to ((x \in A \to \neg x \in B) \leftrightarrow (x \in A \to x \in (C ∖ B)))$
7	1 6	sylbi	$⊢ A \subseteq C \to ((x \in A \to \neg x \in B) \leftrightarrow (x \in A \to x \in (C ∖ B)))$
8	7	albidv	$⊢ A \subseteq C \to (\forall x (x \in A \to \neg x \in B) \leftrightarrow \forall x (x \in A \to x \in (C ∖ B)))$
9		disj1	$⊢ A \cap B = \emptyset \leftrightarrow \forall x (x \in A \to \neg x \in B)$
10		dfss2	$⊢ A \subseteq C ∖ B \leftrightarrow \forall x (x \in A \to x \in (C ∖ B))$
11	8 9 10	3bitr4g	$⊢ A \subseteq C \to (A \cap B = \emptyset \leftrightarrow A \subseteq C ∖ B)$