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

Metamath Proof Explorer

Theorem difun2

Description: Absorption of union by difference. Theorem 36 of Suppes p. 29. (Contributed by NM, 19-May-1998)

		Ref	Expression
	Assertion	difun2	$⊢ (A \cup B) ∖ B = A ∖ B$

Step	Hyp	Ref	Expression
1		difundir	$⊢ (A \cup B) ∖ B = (A ∖ B) \cup (B ∖ B)$
2		difid	$⊢ B ∖ B = \emptyset$
3	2	uneq2i	$⊢ (A ∖ B) \cup (B ∖ B) = (A ∖ B) \cup \emptyset$
4		un0	$⊢ (A ∖ B) \cup \emptyset = A ∖ B$
5	1 3 4	3eqtri	$⊢ (A \cup B) ∖ B = A ∖ B$