This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid 
 |-  ( 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 ) ) )