This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = \emptyset \land B ∖ A = \emptyset) \to A = B$

Step	Hyp	Ref	Expression
1		eqss	$⊢ A = B \leftrightarrow (A \subseteq B \land B \subseteq A)$
2		ssdif0	$⊢ A \subseteq B \leftrightarrow A ∖ B = \emptyset$
3		ssdif0	$⊢ B \subseteq A \leftrightarrow B ∖ A = \emptyset$
4	2 3	anbi12i	$⊢ (A \subseteq B \land B \subseteq A) \leftrightarrow (A ∖ B = \emptyset \land B ∖ A = \emptyset)$
5	1 4	sylbbr	$⊢ (A ∖ B = \emptyset \land B ∖ A = \emptyset) \to A = B$