Metamath Proof Explorer


Theorem resubval

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
|- ( ( A e. RR /\ B e. RR ) -> ( A -R B ) = ( iota_ x e. RR ( B + x ) = A ) )

Proof

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 ) )