disjeq0

Description: Two disjoint sets are equal iff both are empty. (Contributed by AV, 19-Jun-2022)

		Ref	Expression
	Assertion	disjeq0	$⊢ A \cap B = \emptyset \to (A = B \leftrightarrow (A = \emptyset \land B = \emptyset))$

Step	Hyp	Ref	Expression
1		ineq1	$⊢ A = B \to A \cap B = B \cap B$
2		inidm	$⊢ B \cap B = B$
3	1 2	eqtrdi	$⊢ A = B \to A \cap B = B$
4	3	eqeq1d	$⊢ A = B \to (A \cap B = \emptyset \leftrightarrow B = \emptyset)$
5		eqtr	$⊢ (A = B \land B = \emptyset) \to A = \emptyset$
6		simpr	$⊢ (A = B \land B = \emptyset) \to B = \emptyset$
7	5 6	jca	$⊢ (A = B \land B = \emptyset) \to (A = \emptyset \land B = \emptyset)$
8	7	ex	$⊢ A = B \to (B = \emptyset \to (A = \emptyset \land B = \emptyset))$
9	4 8	sylbid	$⊢ A = B \to (A \cap B = \emptyset \to (A = \emptyset \land B = \emptyset))$
10	9	com12	$⊢ A \cap B = \emptyset \to (A = B \to (A = \emptyset \land B = \emptyset))$
11		eqtr3	$⊢ (A = \emptyset \land B = \emptyset) \to A = B$
12	10 11	impbid1	$⊢ A \cap B = \emptyset \to (A = B \leftrightarrow (A = \emptyset \land B = \emptyset))$

Metamath Proof Explorer