Description: Value of real subtraction, which is the (unique) real x such that B + x = A . (Contributed by Steven Nguyen, 7-Jan-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | resubval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq2 | |
|
2 | 1 | riotabidv | |
3 | oveq1 | |
|
4 | 3 | eqeq1d | |
5 | 4 | riotabidv | |
6 | df-resub | |
|
7 | riotaex | |
|
8 | 2 5 6 7 | ovmpo | |