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

Metamath Proof Explorer

Theorem reldisj

Description: Two ways of saying that two classes are disjoint, using the complement of B relative to a universe C . (Contributed by NM, 15-Feb-2007) (Proof shortened by Andrew Salmon, 26-Jun-2011) Avoid ax-12 . (Revised by GG, 28-Jun-2024)

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

Proof

Step	Hyp	Ref	Expression
1		df-ss	$⊢ A \subseteq C \leftrightarrow \forall x (x \in A \to x \in C)$
2		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
3		eleq1w	$⊢ x = y \to (x \in C \leftrightarrow y \in C)$
4	2 3	imbi12d	$⊢ x = y \to ((x \in A \to x \in C) \leftrightarrow (y \in A \to y \in C))$
5	4	spw	$⊢ \forall x (x \in A \to x \in C) \to (x \in A \to x \in C)$
6		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)))$
7		eldif	$⊢ x \in (C ∖ B) \leftrightarrow (x \in C \land \neg x \in B)$
8	7	imbi2i	$⊢ (x \in A \to x \in (C ∖ B)) \leftrightarrow (x \in A \to (x \in C \land \neg x \in B))$
9	6 8	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)))$
10	5 9	syl	$⊢ \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)))$
11	1 10	sylbi	$⊢ A \subseteq C \to ((x \in A \to \neg x \in B) \leftrightarrow (x \in A \to x \in (C ∖ B)))$
12	11	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)))$
13		disj1	$⊢ A \cap B = \emptyset \leftrightarrow \forall x (x \in A \to \neg x \in B)$
14		df-ss	$⊢ A \subseteq C ∖ B \leftrightarrow \forall x (x \in A \to x \in (C ∖ B))$
15	12 13 14	3bitr4g	$⊢ A \subseteq C \to (A \cap B = \emptyset \leftrightarrow A \subseteq C ∖ B)$