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 
|- ( ( A i^i B ) = (/) -> ( A = B <-> ( A = (/) /\ B = (/) ) ) )

Proof

Step Hyp Ref Expression
1 ineq1 
 |-  ( A = B -> ( A i^i B ) = ( B i^i B ) )
2 inidm 
 |-  ( B i^i B ) = B
3 1 2 eqtrdi 
 |-  ( A = B -> ( A i^i B ) = B )
4 3 eqeq1d 
 |-  ( A = B -> ( ( A i^i B ) = (/) <-> B = (/) ) )
5 eqtr 
 |-  ( ( A = B /\ B = (/) ) -> A = (/) )
6 simpr 
 |-  ( ( A = B /\ B = (/) ) -> B = (/) )
7 5 6 jca 
 |-  ( ( A = B /\ B = (/) ) -> ( A = (/) /\ B = (/) ) )
8 7 ex 
 |-  ( A = B -> ( B = (/) -> ( A = (/) /\ B = (/) ) ) )
9 4 8 sylbid 
 |-  ( A = B -> ( ( A i^i B ) = (/) -> ( A = (/) /\ B = (/) ) ) )
10 9 com12 
 |-  ( ( A i^i B ) = (/) -> ( A = B -> ( A = (/) /\ B = (/) ) ) )
11 eqtr3 
 |-  ( ( A = (/) /\ B = (/) ) -> A = B )
12 10 11 impbid1 
 |-  ( ( A i^i B ) = (/) -> ( A = B <-> ( A = (/) /\ B = (/) ) ) )