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 ( 𝐴 ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴

Proof

Step Hyp Ref Expression
1 undif3 ⊢ ( 𝐴 ∪ ( 𝐴 ∖ 𝐵 ) ) = ( ( 𝐴 ∪ 𝐴 ) ∖ ( 𝐵 ∖ 𝐴 ) )
2 unidm ⊢ ( 𝐴 ∪ 𝐴 ) = 𝐴
3 2 difeq1i ⊢ ( ( 𝐴 ∪ 𝐴 ) ∖ ( 𝐵 ∖ 𝐴 ) ) = ( 𝐴 ∖ ( 𝐵 ∖ 𝐴 ) )
4 difdif ⊢ ( 𝐴 ∖ ( 𝐵 ∖ 𝐴 ) ) = 𝐴
5 1 3 4 3eqtri ⊢ ( 𝐴 ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴