undif1

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif ). Theorem 35 of Suppes p. 29. (Contributed by NM, 19-May-1998)

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

Proof

Step	Hyp	Ref	Expression
1		undir	$⊢ (A \cap (V ∖ B)) \cup B = (A \cup B) \cap ((V ∖ B) \cup B)$
2		invdif	$⊢ A \cap (V ∖ B) = A ∖ B$
3	2	uneq1i	$⊢ (A \cap (V ∖ B)) \cup B = (A ∖ B) \cup B$
4		uncom	$⊢ (V ∖ B) \cup B = B \cup (V ∖ B)$
5		unvdif	$⊢ B \cup (V ∖ B) = V$
6	4 5	eqtri	$⊢ (V ∖ B) \cup B = V$
7	6	ineq2i	$⊢ (A \cup B) \cap ((V ∖ B) \cup B) = (A \cup B) \cap V$
8		inv1	$⊢ (A \cup B) \cap V = A \cup B$
9	7 8	eqtri	$⊢ (A \cup B) \cap ((V ∖ B) \cup B) = A \cup B$
10	1 3 9	3eqtr3i	$⊢ (A ∖ B) \cup B = A \cup B$

Metamath Proof Explorer

Theorem undif1

Proof