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\leftrightarrow 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\leftrightarrow 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)$$