Step |
Hyp |
Ref |
Expression |
1 |
|
mptun |
|- ( x e. ( ( A i^i B ) u. ( A \ B ) ) |-> if ( x e. B , C , D ) ) = ( ( x e. ( A i^i B ) |-> if ( x e. B , C , D ) ) u. ( x e. ( A \ B ) |-> if ( x e. B , C , D ) ) ) |
2 |
|
inundif |
|- ( ( A i^i B ) u. ( A \ B ) ) = A |
3 |
|
eqid |
|- if ( x e. B , C , D ) = if ( x e. B , C , D ) |
4 |
2 3
|
mpteq12i |
|- ( x e. ( ( A i^i B ) u. ( A \ B ) ) |-> if ( x e. B , C , D ) ) = ( x e. A |-> if ( x e. B , C , D ) ) |
5 |
|
elinel2 |
|- ( x e. ( A i^i B ) -> x e. B ) |
6 |
5
|
iftrued |
|- ( x e. ( A i^i B ) -> if ( x e. B , C , D ) = C ) |
7 |
6
|
mpteq2ia |
|- ( x e. ( A i^i B ) |-> if ( x e. B , C , D ) ) = ( x e. ( A i^i B ) |-> C ) |
8 |
|
eldifn |
|- ( x e. ( A \ B ) -> -. x e. B ) |
9 |
8
|
iffalsed |
|- ( x e. ( A \ B ) -> if ( x e. B , C , D ) = D ) |
10 |
9
|
mpteq2ia |
|- ( x e. ( A \ B ) |-> if ( x e. B , C , D ) ) = ( x e. ( A \ B ) |-> D ) |
11 |
7 10
|
uneq12i |
|- ( ( x e. ( A i^i B ) |-> if ( x e. B , C , D ) ) u. ( x e. ( A \ B ) |-> if ( x e. B , C , D ) ) ) = ( ( x e. ( A i^i B ) |-> C ) u. ( x e. ( A \ B ) |-> D ) ) |
12 |
1 4 11
|
3eqtr3i |
|- ( x e. A |-> if ( x e. B , C , D ) ) = ( ( x e. ( A i^i B ) |-> C ) u. ( x e. ( A \ B ) |-> D ) ) |