Step |
Hyp |
Ref |
Expression |
1 |
|
cbvditg.1 |
|- ( x = y -> C = D ) |
2 |
|
cbvditg.2 |
|- F/_ y C |
3 |
|
cbvditg.3 |
|- F/_ x D |
4 |
|
biid |
|- ( A <_ B <-> A <_ B ) |
5 |
1 2 3
|
cbvitg |
|- S. ( A (,) B ) C _d x = S. ( A (,) B ) D _d y |
6 |
1 2 3
|
cbvitg |
|- S. ( B (,) A ) C _d x = S. ( B (,) A ) D _d y |
7 |
6
|
negeqi |
|- -u S. ( B (,) A ) C _d x = -u S. ( B (,) A ) D _d y |
8 |
4 5 7
|
ifbieq12i |
|- if ( A <_ B , S. ( A (,) B ) C _d x , -u S. ( B (,) A ) C _d x ) = if ( A <_ B , S. ( A (,) B ) D _d y , -u S. ( B (,) A ) D _d y ) |
9 |
|
df-ditg |
|- S_ [ A -> B ] C _d x = if ( A <_ B , S. ( A (,) B ) C _d x , -u S. ( B (,) A ) C _d x ) |
10 |
|
df-ditg |
|- S_ [ A -> B ] D _d y = if ( A <_ B , S. ( A (,) B ) D _d y , -u S. ( B (,) A ) D _d y ) |
11 |
8 9 10
|
3eqtr4i |
|- S_ [ A -> B ] C _d x = S_ [ A -> B ] D _d y |