disjex

Description: Two ways to say that two classes are disjoint (or equal). (Contributed by Thierry Arnoux, 4-Oct-2016)

		Ref	Expression
	Assertion	disjex	$⊢ (\exists z (z \in A \land z \in B) \to A = B) \leftrightarrow (A = B \lor A \cap B = \emptyset)$

Step	Hyp	Ref	Expression
1		orcom	$⊢ (A = B \lor \neg \exists z (z \in A \land z \in B)) \leftrightarrow (\neg \exists z (z \in A \land z \in B) \lor A = B)$
2		df-in	$⊢ A \cap B = \{z \| (z \in A \land z \in B)\}$
3	2	neeq1i	$⊢ A \cap B \neq \emptyset \leftrightarrow \{z \| (z \in A \land z \in B)\} \neq \emptyset$
4		abn0	$⊢ \{z \| (z \in A \land z \in B)\} \neq \emptyset \leftrightarrow \exists z (z \in A \land z \in B)$
5	3 4	bitr2i	$⊢ \exists z (z \in A \land z \in B) \leftrightarrow A \cap B \neq \emptyset$
6	5	necon2bbii	$⊢ A \cap B = \emptyset \leftrightarrow \neg \exists z (z \in A \land z \in B)$
7	6	orbi2i	$⊢ (A = B \lor A \cap B = \emptyset) \leftrightarrow (A = B \lor \neg \exists z (z \in A \land z \in B))$
8		imor	$⊢ (\exists z (z \in A \land z \in B) \to A = B) \leftrightarrow (\neg \exists z (z \in A \land z \in B) \lor A = B)$
9	1 7 8	3bitr4ri	$⊢ (\exists z (z \in A \land z \in B) \to A = B) \leftrightarrow (A = B \lor A \cap B = \emptyset)$

Metamath Proof Explorer