disjexc

Description: A variant of disjex , applicable for more generic families. (Contributed by Thierry Arnoux, 4-Oct-2016)

		Ref	Expression
	Hypothesis	disjexc.1	$⊢ x = y \to A = B$
	Assertion	disjexc	$⊢ (\exists z (z \in A \land z \in B) \to x = y) \to (A = B \lor A \cap B = \emptyset)$

Step	Hyp	Ref	Expression
1		disjexc.1	$⊢ x = y \to A = B$
2	1	imim2i	$⊢ (\exists z (z \in A \land z \in B) \to x = y) \to (\exists z (z \in A \land z \in B) \to A = B)$
3		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)$
4		df-in	$⊢ A \cap B = \{z \| (z \in A \land z \in B)\}$
5	4	neeq1i	$⊢ A \cap B \neq \emptyset \leftrightarrow \{z \| (z \in A \land z \in B)\} \neq \emptyset$
6		abn0	$⊢ \{z \| (z \in A \land z \in B)\} \neq \emptyset \leftrightarrow \exists z (z \in A \land z \in B)$
7	5 6	bitr2i	$⊢ \exists z (z \in A \land z \in B) \leftrightarrow A \cap B \neq \emptyset$
8	7	necon2bbii	$⊢ A \cap B = \emptyset \leftrightarrow \neg \exists z (z \in A \land z \in B)$
9	8	orbi2i	$⊢ (A = B \lor A \cap B = \emptyset) \leftrightarrow (A = B \lor \neg \exists z (z \in A \land z \in B))$
10		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)$
11	3 9 10	3bitr4i	$⊢ (A = B \lor A \cap B = \emptyset) \leftrightarrow (\exists z (z \in A \land z \in B) \to A = B)$
12	2 11	sylibr	$⊢ (\exists z (z \in A \land z \in B) \to x = y) \to (A = B \lor A \cap B = \emptyset)$

Metamath Proof Explorer