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

Metamath Proof Explorer

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

Proof

Step	Hyp	Ref	Expression
1		undir	⊢ ( ( 𝐴 ∩ ( V ∖ 𝐵 ) ) ∪ 𝐵 ) = ( ( 𝐴 ∪ 𝐵 ) ∩ ( ( V ∖ 𝐵 ) ∪ 𝐵 ) )
2		invdif	⊢ ( 𝐴 ∩ ( V ∖ 𝐵 ) ) = ( 𝐴 ∖ 𝐵 )
3	2	uneq1i	⊢ ( ( 𝐴 ∩ ( V ∖ 𝐵 ) ) ∪ 𝐵 ) = ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 )
4		uncom	⊢ ( ( V ∖ 𝐵 ) ∪ 𝐵 ) = ( 𝐵 ∪ ( V ∖ 𝐵 ) )
5		unvdif	⊢ ( 𝐵 ∪ ( V ∖ 𝐵 ) ) = V
6	4 5	eqtri	⊢ ( ( V ∖ 𝐵 ) ∪ 𝐵 ) = V
7	6	ineq2i	⊢ ( ( 𝐴 ∪ 𝐵 ) ∩ ( ( V ∖ 𝐵 ) ∪ 𝐵 ) ) = ( ( 𝐴 ∪ 𝐵 ) ∩ V )
8		inv1	⊢ ( ( 𝐴 ∪ 𝐵 ) ∩ V ) = ( 𝐴 ∪ 𝐵 )
9	7 8	eqtri	⊢ ( ( 𝐴 ∪ 𝐵 ) ∩ ( ( V ∖ 𝐵 ) ∪ 𝐵 ) ) = ( 𝐴 ∪ 𝐵 )
10	1 3 9	3eqtr3i	⊢ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) = ( 𝐴 ∪ 𝐵 )