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

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