Theorem disjeq0

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

	Ref	Expression
Assertion	disjeq0	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐴 = 𝐵 ↔ ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ) )

Proof

Step	Hyp	Ref	Expression
1		ineq1	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐵 ) )
2		inidm	⊢ ( 𝐵 ∩ 𝐵 ) = 𝐵
3	1 2	eqtrdi	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∩ 𝐵 ) = 𝐵 )
4	3	eqeq1d	⊢ ( 𝐴 = 𝐵 → ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ 𝐵 = ∅ ) )
5		eqtr	⊢ ( ( 𝐴 = 𝐵 ∧ 𝐵 = ∅ ) → 𝐴 = ∅ )
6		simpr	⊢ ( ( 𝐴 = 𝐵 ∧ 𝐵 = ∅ ) → 𝐵 = ∅ )
7	5 6	jca	⊢ ( ( 𝐴 = 𝐵 ∧ 𝐵 = ∅ ) → ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) )
8	7	ex	⊢ ( 𝐴 = 𝐵 → ( 𝐵 = ∅ → ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ) )
9	4 8	sylbid	⊢ ( 𝐴 = 𝐵 → ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ) )
10	9	com12	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐴 = 𝐵 → ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ) )
11		eqtr3	⊢ ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) → 𝐴 = 𝐵 )
12	10 11	impbid1	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐴 = 𝐵 ↔ ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ) )