Theorem difdif2

Description: Class difference by a class difference. (Contributed by Thierry Arnoux, 18-Dec-2017)

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

Proof

Step	Hyp	Ref	Expression
1		difindi	|- ( A \ ( B i^i ( _V \ C ) ) ) = ( ( A \ B ) u. ( A \ ( _V \ C ) ) )
2		invdif	|- ( B i^i ( _V \ C ) ) = ( B \ C )
3	2	eqcomi	|- ( B \ C ) = ( B i^i ( _V \ C ) )
4	3	difeq2i	|- ( A \ ( B \ C ) ) = ( A \ ( B i^i ( _V \ C ) ) )
5		dfin2	|- ( A i^i C ) = ( A \ ( _V \ C ) )
6	5	uneq2i	|- ( ( A \ B ) u. ( A i^i C ) ) = ( ( A \ B ) u. ( A \ ( _V \ C ) ) )
7	1 4 6	3eqtr4i	|- ( A \ ( B \ C ) ) = ( ( A \ B ) u. ( A i^i C ) )