# 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 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}-{B}=\left(\iota {x}\in ℂ|{B}+{x}={A}\right)$

### Proof

Step Hyp Ref Expression
1 eqeq2 ${⊢}{y}={A}\to \left({z}+{x}={y}↔{z}+{x}={A}\right)$
2 1 riotabidv ${⊢}{y}={A}\to \left(\iota {x}\in ℂ|{z}+{x}={y}\right)=\left(\iota {x}\in ℂ|{z}+{x}={A}\right)$
3 oveq1 ${⊢}{z}={B}\to {z}+{x}={B}+{x}$
4 3 eqeq1d ${⊢}{z}={B}\to \left({z}+{x}={A}↔{B}+{x}={A}\right)$
5 4 riotabidv ${⊢}{z}={B}\to \left(\iota {x}\in ℂ|{z}+{x}={A}\right)=\left(\iota {x}\in ℂ|{B}+{x}={A}\right)$
6 df-sub ${⊢}-=\left({y}\in ℂ,{z}\in ℂ⟼\left(\iota {x}\in ℂ|{z}+{x}={y}\right)\right)$
7 riotaex ${⊢}\left(\iota {x}\in ℂ|{B}+{x}={A}\right)\in \mathrm{V}$
8 2 5 6 7 ovmpo ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}-{B}=\left(\iota {x}\in ℂ|{B}+{x}={A}\right)$