Theorem difundi

Description: Distributive law for class difference. Theorem 39 of Suppes p. 29. (Contributed by NM, 17-Aug-2004)

	Ref	Expression
Assertion	difundi	|- ( A \ ( B u. C ) ) = ( ( A \ B ) i^i ( A \ C ) )

Proof

Step	Hyp	Ref	Expression
1		dfun3	|- ( B u. C ) = ( _V \ ( ( _V \ B ) i^i ( _V \ C ) ) )
2	1	difeq2i	|- ( A \ ( B u. C ) ) = ( A \ ( _V \ ( ( _V \ B ) i^i ( _V \ C ) ) ) )
3		inindi	|- ( A i^i ( ( _V \ B ) i^i ( _V \ C ) ) ) = ( ( A i^i ( _V \ B ) ) i^i ( A i^i ( _V \ C ) ) )
4		dfin2	|- ( A i^i ( ( _V \ B ) i^i ( _V \ C ) ) ) = ( A \ ( _V \ ( ( _V \ B ) i^i ( _V \ C ) ) ) )
5		invdif	|- ( A i^i ( _V \ B ) ) = ( A \ B )
6		invdif	|- ( A i^i ( _V \ C ) ) = ( A \ C )
7	5 6	ineq12i	|- ( ( A i^i ( _V \ B ) ) i^i ( A i^i ( _V \ C ) ) ) = ( ( A \ B ) i^i ( A \ C ) )
8	3 4 7	3eqtr3i	|- ( A \ ( _V \ ( ( _V \ B ) i^i ( _V \ C ) ) ) ) = ( ( A \ B ) i^i ( A \ C ) )
9	2 8	eqtri	|- ( A \ ( B u. C ) ) = ( ( A \ B ) i^i ( A \ C ) )