Metamath Proof Explorer


Theorem subval

Description: Value of subtraction, which is the (unique) element x such that B + x = A . (Contributed by NM, 4-Aug-2007) (Revised by Mario Carneiro, 2-Nov-2013)

Ref Expression
Assertion subval A B A B = ι x | B + x = A

Proof

Step Hyp Ref Expression
1 eqeq2 y = A z + x = y z + x = A
2 1 riotabidv y = A ι x | z + x = y = ι x | 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 ι x | z + x = A = ι x | B + x = A
6 df-sub = y , z ι x | z + x = y
7 riotaex ι x | B + x = A V
8 2 5 6 7 ovmpo A B A B = ι x | B + x = A