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

Proof

Step	Hyp	Ref	Expression
1		eqss	⊢ ( 𝐴 = 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) )
2		ssdif0	⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∖ 𝐵 ) = ∅ )
3		ssdif0	⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐵 ∖ 𝐴 ) = ∅ )
4	2 3	anbi12i	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) ↔ ( ( 𝐴 ∖ 𝐵 ) = ∅ ∧ ( 𝐵 ∖ 𝐴 ) = ∅ ) )
5	1 4	sylbbr	⊢ ( ( ( 𝐴 ∖ 𝐵 ) = ∅ ∧ ( 𝐵 ∖ 𝐴 ) = ∅ ) → 𝐴 = 𝐵 )