Theorem difuncomp

Description: Express a class difference using unions and class complements. (Contributed by Thierry Arnoux, 21-Jun-2020)

	Ref	Expression
Assertion	difuncomp	|- ( A C_ C -> ( A \ B ) = ( C \ ( ( C \ A ) u. B ) ) )

Proof

Step	Hyp	Ref	Expression
1		sseqin2	|- ( A C_ C <-> ( C i^i A ) = A )
2	1	biimpi	|- ( A C_ C -> ( C i^i A ) = A )
3		incom	|- ( C i^i A ) = ( A i^i C )
4	2 3	eqtr3di	|- ( A C_ C -> A = ( A i^i C ) )
5	4	difeq1d	|- ( A C_ C -> ( A \ B ) = ( ( A i^i C ) \ B ) )
6		difundi	|- ( C \ ( ( C \ A ) u. B ) ) = ( ( C \ ( C \ A ) ) i^i ( C \ B ) )
7		dfss4	|- ( A C_ C <-> ( C \ ( C \ A ) ) = A )
8	7	biimpi	|- ( A C_ C -> ( C \ ( C \ A ) ) = A )
9	8	ineq1d	|- ( A C_ C -> ( ( C \ ( C \ A ) ) i^i ( C \ B ) ) = ( A i^i ( C \ B ) ) )
10	6 9	syl5eq	|- ( A C_ C -> ( C \ ( ( C \ A ) u. B ) ) = ( A i^i ( C \ B ) ) )
11		indif2	|- ( A i^i ( C \ B ) ) = ( ( A i^i C ) \ B )
12	10 11	eqtrdi	|- ( A C_ C -> ( C \ ( ( C \ A ) u. B ) ) = ( ( A i^i C ) \ B ) )
13	5 12	eqtr4d	|- ( A C_ C -> ( A \ B ) = ( C \ ( ( C \ A ) u. B ) ) )