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	$$⊢\left(A\setminus B=\varnothing \wedge B\setminus A=\varnothing \right)\to A=B$$

Proof

Step	Hyp	Ref	Expression
1		eqss	$$⊢A=B\leftrightarrow \left(A\subseteq B\wedge B\subseteq A\right)$$
2		ssdif0	$$⊢A\subseteq B\leftrightarrow A\setminus B=\varnothing$$
3		ssdif0	$$⊢B\subseteq A\leftrightarrow B\setminus A=\varnothing$$
4	2 3	anbi12i	$$⊢\left(A\subseteq B\wedge B\subseteq A\right)\leftrightarrow \left(A\setminus B=\varnothing \wedge B\setminus A=\varnothing \right)$$
5	1 4	sylbbr	$$⊢\left(A\setminus B=\varnothing \wedge B\setminus A=\varnothing \right)\to A=B$$