# 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 ${⊢}{A}\cap {B}=\varnothing \to \left({A}={B}↔\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 syl6eq ${⊢}{A}={B}\to {A}\cap {B}={B}$
4 3 eqeq1d ${⊢}{A}={B}\to \left({A}\cap {B}=\varnothing ↔{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}↔\left({A}=\varnothing \wedge {B}=\varnothing \right)\right)$