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 = \{z \| (z \in A \land z \in B)\}$
2	1	eqeq1i	$⊢ A \cap B = \emptyset \leftrightarrow \{z \| (z \in A \land z \in B)\} = \emptyset$
3		dfcleq	$⊢ \emptyset = \{z \| (z \in A \land z \in B)\} \leftrightarrow \forall x (x \in \emptyset \leftrightarrow x \in \{z \| (z \in A \land z \in B)\})$
4		df-clab	$⊢ x \in \{z \| (z \in A \land z \in B)\} \leftrightarrow [x/ z] (z \in A \land z \in B)$
5		sb6	$⊢ [x/ z] (z \in A \land z \in B) \leftrightarrow \forall z (z = x \to (z \in A \land z \in B))$
6		id	$⊢ z = x \to z = x$
7		eleq1w	$⊢ z = x \to (z \in A \leftrightarrow x \in A)$
8	7	biimpd	$⊢ z = x \to (z \in A \to x \in A)$
9		eleq1w	$⊢ z = x \to (z \in B \leftrightarrow x \in B)$
10	9	biimpd	$⊢ z = x \to (z \in B \to x \in B)$
11	8 10	anim12d	$⊢ z = x \to ((z \in A \land z \in B) \to (x \in A \land x \in B))$
12	6 11	embantd	$⊢ z = x \to ((z = x \to (z \in A \land z \in B)) \to (x \in A \land x \in B))$
13	12	spimvw	$⊢ \forall z (z = x \to (z \in A \land z \in B)) \to (x \in A \land x \in B)$
14		eleq1a	$⊢ x \in A \to (z = x \to z \in A)$
15		eleq1a	$⊢ x \in B \to (z = x \to z \in B)$
16	14 15	anim12ii	$⊢ (x \in A \land x \in B) \to (z = x \to (z \in A \land z \in B))$
17	16	alrimiv	$⊢ (x \in A \land x \in B) \to \forall z (z = x \to (z \in A \land z \in B))$
18	13 17	impbii	$⊢ \forall z (z = x \to (z \in A \land z \in B)) \leftrightarrow (x \in A \land x \in B)$
19	4 5 18	3bitri	$⊢ x \in \{z \| (z \in A \land z \in B)\} \leftrightarrow (x \in A \land x \in B)$
20	19	bibi2i	$⊢ (x \in \emptyset \leftrightarrow x \in \{z \| (z \in A \land z \in B)\}) \leftrightarrow (x \in \emptyset \leftrightarrow (x \in A \land x \in B))$
21	20	albii	$⊢ \forall x (x \in \emptyset \leftrightarrow x \in \{z \| (z \in A \land z \in B)\}) \leftrightarrow \forall x (x \in \emptyset \leftrightarrow (x \in A \land x \in B))$
22	3 21	bitri	$⊢ \emptyset = \{z \| (z \in A \land z \in B)\} \leftrightarrow \forall x (x \in \emptyset \leftrightarrow (x \in A \land x \in B))$
23		eqcom	$⊢ \{z \| (z \in A \land z \in B)\} = \emptyset \leftrightarrow \emptyset = \{z \| (z \in A \land z \in B)\}$
24		bicom	$⊢ ((x \in A \land x \in B) \leftrightarrow x \in \emptyset) \leftrightarrow (x \in \emptyset \leftrightarrow (x \in A \land x \in B))$
25	24	albii	$⊢ \forall x ((x \in A \land x \in B) \leftrightarrow x \in \emptyset) \leftrightarrow \forall x (x \in \emptyset \leftrightarrow (x \in A \land x \in B))$
26	22 23 25	3bitr4i	$⊢ \{z \| (z \in A \land z \in B)\} = \emptyset \leftrightarrow \forall x ((x \in A \land x \in B) \leftrightarrow x \in \emptyset)$
27		imnan	$⊢ (x \in A \to \neg x \in B) \leftrightarrow \neg (x \in A \land x \in B)$
28		noel	$⊢ \neg x \in \emptyset$
29	28	nbn	$⊢ \neg (x \in A \land x \in B) \leftrightarrow ((x \in A \land x \in B) \leftrightarrow x \in \emptyset)$
30	27 29	bitr2i	$⊢ ((x \in A \land x \in B) \leftrightarrow x \in \emptyset) \leftrightarrow (x \in A \to \neg x \in B)$
31	30	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)$
32	2 26 31	3bitri	$⊢ A \cap B = \emptyset \leftrightarrow \forall x (x \in A \to \neg x \in B)$
33		df-ral	$⊢ \forall x \in A \neg x \in B \leftrightarrow \forall x (x \in A \to \neg x \in B)$
34	32 33	bitr4i	$⊢ A \cap B = \emptyset \leftrightarrow \forall x \in A \neg x \in B$

Metamath Proof Explorer

Theorem disj

Proof