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

Metamath Proof Explorer

Theorem undif5

Description: An equality involving class union and class difference. (Contributed by Thierry Arnoux, 26-Jun-2024)

		Ref	Expression
	Assertion	undif5	$⊢ A \cap B = \emptyset \to (A \cup B) ∖ B = A$

Step	Hyp	Ref	Expression
1		difun2	$⊢ (A \cup B) ∖ B = A ∖ B$
2		disjdif2	$⊢ A \cap B = \emptyset \to A ∖ B = A$
3	1 2	eqtrid	$⊢ A \cap B = \emptyset \to (A \cup B) ∖ B = A$