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	$$⊢\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-resub	$$⊢{-}_{ℝ}=\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)$$