disj3

Description: Two ways of saying that two classes are disjoint. (Contributed by NM, 19-May-1998)

		Ref	Expression
	Assertion	disj3	$⊢ A \cap B = \emptyset \leftrightarrow A = A ∖ B$

Step	Hyp	Ref	Expression
1		pm4.71	$⊢ (x \in A \to \neg x \in B) \leftrightarrow (x \in A \leftrightarrow (x \in A \land \neg x \in B))$
2		eldif	$⊢ x \in (A ∖ B) \leftrightarrow (x \in A \land \neg x \in B)$
3	2	bibi2i	$⊢ (x \in A \leftrightarrow x \in (A ∖ B)) \leftrightarrow (x \in A \leftrightarrow (x \in A \land \neg x \in B))$
4	1 3	bitr4i	$⊢ (x \in A \to \neg x \in B) \leftrightarrow (x \in A \leftrightarrow x \in (A ∖ B))$
5	4	albii	$⊢ \forall x (x \in A \to \neg x \in B) \leftrightarrow \forall x (x \in A \leftrightarrow x \in (A ∖ B))$
6		disj1	$⊢ A \cap B = \emptyset \leftrightarrow \forall x (x \in A \to \neg x \in B)$
7		dfcleq	$⊢ A = A ∖ B \leftrightarrow \forall x (x \in A \leftrightarrow x \in (A ∖ B))$
8	5 6 7	3bitr4i	$⊢ A \cap B = \emptyset \leftrightarrow A = A ∖ B$

Metamath Proof Explorer