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

Metamath Proof Explorer

Theorem undifabs

Description: Absorption of difference by union. (Contributed by NM, 18-Aug-2013)

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

Proof

Step Hyp Ref Expression
1 undif3 ⊢ A ∪ A ∖ B = A ∪ A ∖ B ∖ A
2 unidm ⊢ A ∪ A = A
3 2 difeq1i ⊢ A ∪ A ∖ B ∖ A = A ∖ B ∖ A
4 difdif ⊢ A ∖ B ∖ A = A
5 1 3 4 3eqtri ⊢ A ∪ A ∖ B = A