Step |
Hyp |
Ref |
Expression |
1 |
|
eqeq1 |
|- ( A = B -> ( A = +oo <-> B = +oo ) ) |
2 |
|
eqeq1 |
|- ( A = B -> ( A = -oo <-> B = -oo ) ) |
3 |
|
negeq |
|- ( A = B -> -u A = -u B ) |
4 |
2 3
|
ifbieq2d |
|- ( A = B -> if ( A = -oo , +oo , -u A ) = if ( B = -oo , +oo , -u B ) ) |
5 |
1 4
|
ifbieq2d |
|- ( A = B -> if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) ) = if ( B = +oo , -oo , if ( B = -oo , +oo , -u B ) ) ) |
6 |
|
df-xneg |
|- -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) ) |
7 |
|
df-xneg |
|- -e B = if ( B = +oo , -oo , if ( B = -oo , +oo , -u B ) ) |
8 |
5 6 7
|
3eqtr4g |
|- ( A = B -> -e A = -e B ) |