Step |
Hyp |
Ref |
Expression |
1 |
|
eqeq2 |
|- ( y = A -> ( ( z + x ) = y <-> ( z + x ) = A ) ) |
2 |
1
|
riotabidv |
|- ( y = A -> ( iota_ x e. RR ( z + x ) = y ) = ( iota_ x e. RR ( z + x ) = A ) ) |
3 |
|
oveq1 |
|- ( z = B -> ( z + x ) = ( B + x ) ) |
4 |
3
|
eqeq1d |
|- ( z = B -> ( ( z + x ) = A <-> ( B + x ) = A ) ) |
5 |
4
|
riotabidv |
|- ( z = B -> ( iota_ x e. RR ( z + x ) = A ) = ( iota_ x e. RR ( B + x ) = A ) ) |
6 |
|
df-resub |
|- -R = ( y e. RR , z e. RR |-> ( iota_ x e. RR ( z + x ) = y ) ) |
7 |
|
riotaex |
|- ( iota_ x e. RR ( B + x ) = A ) e. _V |
8 |
2 5 6 7
|
ovmpo |
|- ( ( A e. RR /\ B e. RR ) -> ( A -R B ) = ( iota_ x e. RR ( B + x ) = A ) ) |