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 ABA-B=ιx|B+x=A

Proof

Step Hyp Ref Expression
1 eqeq2 y=Az+x=yz+x=A
2 1 riotabidv y=Aιx|z+x=y=ιx|z+x=A
3 oveq1 z=Bz+x=B+x
4 3 eqeq1d z=Bz+x=AB+x=A
5 4 riotabidv z=Bιx|z+x=A=ιx|B+x=A
6 df-resub -=y,zιx|z+x=y
7 riotaex ιx|B+x=AV
8 2 5 6 7 ovmpo ABA-B=ιx|B+x=A