Theorem disjeq0

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

	Ref	Expression
Assertion	disjeq0	$$⊢A\cap B=\varnothing \to \left(A=B\leftrightarrow \left(A=\varnothing \wedge B=\varnothing \right)\right)$$

Proof

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 \left(A\cap B=\varnothing \leftrightarrow B=\varnothing \right)$$
5		eqtr	$$⊢\left(A=B\wedge B=\varnothing \right)\to A=\varnothing$$
6		simpr	$$⊢\left(A=B\wedge B=\varnothing \right)\to B=\varnothing$$
7	5 6	jca	$$⊢\left(A=B\wedge B=\varnothing \right)\to \left(A=\varnothing \wedge B=\varnothing \right)$$
8	7	ex	$$⊢A=B\to \left(B=\varnothing \to \left(A=\varnothing \wedge B=\varnothing \right)\right)$$
9	4 8	sylbid	$$⊢A=B\to \left(A\cap B=\varnothing \to \left(A=\varnothing \wedge B=\varnothing \right)\right)$$
10	9	com12	$$⊢A\cap B=\varnothing \to \left(A=B\to \left(A=\varnothing \wedge B=\varnothing \right)\right)$$
11		eqtr3	$$⊢\left(A=\varnothing \wedge B=\varnothing \right)\to A=B$$
12	10 11	impbid1	$$⊢A\cap B=\varnothing \to \left(A=B\leftrightarrow \left(A=\varnothing \wedge B=\varnothing \right)\right)$$