# 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)$
{"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 9, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0}