Step |
Hyp |
Ref |
Expression |
1 |
|
iccshftri.1 |
|- A e. RR |
2 |
|
iccshftri.2 |
|- B e. RR |
3 |
|
iccshftri.3 |
|- R e. RR |
4 |
|
iccshftri.4 |
|- ( A + R ) = C |
5 |
|
iccshftri.5 |
|- ( B + R ) = D |
6 |
|
iccssre |
|- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR ) |
7 |
1 2 6
|
mp2an |
|- ( A [,] B ) C_ RR |
8 |
7
|
sseli |
|- ( X e. ( A [,] B ) -> X e. RR ) |
9 |
4 5
|
iccshftr |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ R e. RR ) ) -> ( X e. ( A [,] B ) <-> ( X + R ) e. ( C [,] D ) ) ) |
10 |
1 2 9
|
mpanl12 |
|- ( ( X e. RR /\ R e. RR ) -> ( X e. ( A [,] B ) <-> ( X + R ) e. ( C [,] D ) ) ) |
11 |
3 10
|
mpan2 |
|- ( X e. RR -> ( X e. ( A [,] B ) <-> ( X + R ) e. ( C [,] D ) ) ) |
12 |
11
|
biimpd |
|- ( X e. RR -> ( X e. ( A [,] B ) -> ( X + R ) e. ( C [,] D ) ) ) |
13 |
8 12
|
mpcom |
|- ( X e. ( A [,] B ) -> ( X + R ) e. ( C [,] D ) ) |