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	|- ( ( A \ B ) u. B ) = ( A u. B )

Proof

Step	Hyp	Ref	Expression
1		undir	|- ( ( A i^i ( _V \ B ) ) u. B ) = ( ( A u. B ) i^i ( ( _V \ B ) u. B ) )
2		invdif	|- ( A i^i ( _V \ B ) ) = ( A \ B )
3	2	uneq1i	|- ( ( A i^i ( _V \ B ) ) u. B ) = ( ( A \ B ) u. B )
4		uncom	|- ( ( _V \ B ) u. B ) = ( B u. ( _V \ B ) )
5		unvdif	|- ( B u. ( _V \ B ) ) = _V
6	4 5	eqtri	|- ( ( _V \ B ) u. B ) = _V
7	6	ineq2i	|- ( ( A u. B ) i^i ( ( _V \ B ) u. B ) ) = ( ( A u. B ) i^i _V )
8		inv1	|- ( ( A u. B ) i^i _V ) = ( A u. B )
9	7 8	eqtri	|- ( ( A u. B ) i^i ( ( _V \ B ) u. B ) ) = ( A u. B )
10	1 3 9	3eqtr3i	|- ( ( A \ B ) u. B ) = ( A u. B )