This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐴 = 𝐵 ↔ ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ) )