Metamath Proof Explorer

Theorem disj

Description: Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004) Avoid ax-10 , ax-11 , ax-12 . (Revised by GG, 28-Jun-2024)

		Ref	Expression
	Assertion	disj	$⊢ A \cap B = \emptyset \leftrightarrow \forall x \in A \neg x \in B$

Proof

Step	Hyp	Ref	Expression
1		df-in	$⊢ A \cap B = \{y \| (y \in A \land y \in B)\}$
2	1	eqeq1i	$⊢ A \cap B = \emptyset \leftrightarrow \{y \| (y \in A \land y \in B)\} = \emptyset$
3		eleq1w	$⊢ y = x \to (y \in A \leftrightarrow x \in A)$
4		eleq1w	$⊢ y = x \to (y \in B \leftrightarrow x \in B)$
5	3 4	anbi12d	$⊢ y = x \to ((y \in A \land y \in B) \leftrightarrow (x \in A \land x \in B))$
6	5	eqabcbw	$⊢ \{y \| (y \in A \land y \in B)\} = \emptyset \leftrightarrow \forall x ((x \in A \land x \in B) \leftrightarrow x \in \emptyset)$
7		imnan	$⊢ (x \in A \to \neg x \in B) \leftrightarrow \neg (x \in A \land x \in B)$
8		noel	$⊢ \neg x \in \emptyset$
9	8	nbn	$⊢ \neg (x \in A \land x \in B) \leftrightarrow ((x \in A \land x \in B) \leftrightarrow x \in \emptyset)$
10	7 9	bitr2i	$⊢ ((x \in A \land x \in B) \leftrightarrow x \in \emptyset) \leftrightarrow (x \in A \to \neg x \in B)$
11	10	albii	$⊢ \forall x ((x \in A \land x \in B) \leftrightarrow x \in \emptyset) \leftrightarrow \forall x (x \in A \to \neg x \in B)$
12	2 6 11	3bitri	$⊢ A \cap B = \emptyset \leftrightarrow \forall x (x \in A \to \neg x \in B)$
13		df-ral	$⊢ \forall x \in A \neg x \in B \leftrightarrow \forall x (x \in A \to \neg x \in B)$
14	12 13	bitr4i	$⊢ A \cap B = \emptyset \leftrightarrow \forall x \in A \neg x \in B$