Theorem difdifdir

Description: Distributive law for class difference. Exercise 4.8 of Stoll p. 16. (Contributed by NM, 18-Aug-2004)

	Ref	Expression
Assertion	difdifdir	|- ( ( A \ B ) \ C ) = ( ( A \ C ) \ ( B \ C ) )

Proof

Step	Hyp	Ref	Expression
1		dif32	|- ( ( A \ B ) \ C ) = ( ( A \ C ) \ B )
2		invdif	|- ( ( A \ C ) i^i ( _V \ B ) ) = ( ( A \ C ) \ B )
3	1 2	eqtr4i	|- ( ( A \ B ) \ C ) = ( ( A \ C ) i^i ( _V \ B ) )
4		un0	|- ( ( ( A \ C ) i^i ( _V \ B ) ) u. (/) ) = ( ( A \ C ) i^i ( _V \ B ) )
5	3 4	eqtr4i	|- ( ( A \ B ) \ C ) = ( ( ( A \ C ) i^i ( _V \ B ) ) u. (/) )
6		indi	|- ( ( A \ C ) i^i ( ( _V \ B ) u. C ) ) = ( ( ( A \ C ) i^i ( _V \ B ) ) u. ( ( A \ C ) i^i C ) )
7		disjdif	|- ( C i^i ( A \ C ) ) = (/)
8		incom	|- ( C i^i ( A \ C ) ) = ( ( A \ C ) i^i C )
9	7 8	eqtr3i	|- (/) = ( ( A \ C ) i^i C )
10	9	uneq2i	|- ( ( ( A \ C ) i^i ( _V \ B ) ) u. (/) ) = ( ( ( A \ C ) i^i ( _V \ B ) ) u. ( ( A \ C ) i^i C ) )
11	6 10	eqtr4i	|- ( ( A \ C ) i^i ( ( _V \ B ) u. C ) ) = ( ( ( A \ C ) i^i ( _V \ B ) ) u. (/) )
12	5 11	eqtr4i	|- ( ( A \ B ) \ C ) = ( ( A \ C ) i^i ( ( _V \ B ) u. C ) )
13		ddif	|- ( _V \ ( _V \ C ) ) = C
14	13	uneq2i	|- ( ( _V \ B ) u. ( _V \ ( _V \ C ) ) ) = ( ( _V \ B ) u. C )
15		indm	|- ( _V \ ( B i^i ( _V \ C ) ) ) = ( ( _V \ B ) u. ( _V \ ( _V \ C ) ) )
16		invdif	|- ( B i^i ( _V \ C ) ) = ( B \ C )
17	16	difeq2i	|- ( _V \ ( B i^i ( _V \ C ) ) ) = ( _V \ ( B \ C ) )
18	15 17	eqtr3i	|- ( ( _V \ B ) u. ( _V \ ( _V \ C ) ) ) = ( _V \ ( B \ C ) )
19	14 18	eqtr3i	|- ( ( _V \ B ) u. C ) = ( _V \ ( B \ C ) )
20	19	ineq2i	|- ( ( A \ C ) i^i ( ( _V \ B ) u. C ) ) = ( ( A \ C ) i^i ( _V \ ( B \ C ) ) )
21		invdif	|- ( ( A \ C ) i^i ( _V \ ( B \ C ) ) ) = ( ( A \ C ) \ ( B \ C ) )
22	12 20 21	3eqtri	|- ( ( A \ B ) \ C ) = ( ( A \ C ) \ ( B \ C ) )