Metamath Proof Explorer

Theorem eqdif

Description: If both set differences of two sets are empty, those sets are equal. (Contributed by Thierry Arnoux, 16-Nov-2023)

Ref Expression
Assertion eqdif 
|- ( ( ( A \ B ) = (/) /\ ( B \ A ) = (/) ) -> A = B )

Proof

Step Hyp Ref Expression
1 eqss 
 |-  ( A = B <-> ( A C_ B /\ B C_ A ) )
2 ssdif0 
 |-  ( A C_ B <-> ( A \ B ) = (/) )
3 ssdif0 
 |-  ( B C_ A <-> ( B \ A ) = (/) )
4 2 3 anbi12i 
 |-  ( ( A C_ B /\ B C_ A ) <-> ( ( A \ B ) = (/) /\ ( B \ A ) = (/) ) )
5 1 4 sylbbr 
 |-  ( ( ( A \ B ) = (/) /\ ( B \ A ) = (/) ) -> A = B )