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

Metamath Proof Explorer

Theorem undif2

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif ). Part of proof of Corollary 6K of Enderton p. 144. (Contributed by NM, 19-May-1998)

Ref Expression
Assertion undif2 ⊢ A ∪ B ∖ A = A ∪ B

Proof

Step Hyp Ref Expression
1 uncom ⊢ A ∪ B ∖ A = B ∖ A ∪ A
2 undif1 ⊢ B ∖ A ∪ A = B ∪ A
3 uncom ⊢ B ∪ A = A ∪ B
4 1 2 3 3eqtri ⊢ A ∪ B ∖ A = A ∪ B