Definition df-resub

Description: Define subtraction between real numbers. This operator saves a few axioms over df-sub in certain situations. Theorem resubval shows its value, resubadd relates it to addition, and rersubcl proves its closure. It is the restriction of df-sub to the reals: subresre . (Contributed by Steven Nguyen, 7-Jan-2023)

	Ref	Expression
Assertion	df-resub	$$⊢{-}_{ℝ}=\left(x\in ℝ,y\in ℝ⟼\left(\iota z\in ℝ|y+z=x\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cresub	$$class{-}_{ℝ}$$
1		vx	$$setvarx$$
2		cr	$$classℝ$$
3		vy	$$setvary$$
4		vz	$$setvarz$$
5	3	cv	$$setvary$$
6		caddc	$$class+$$
7	4	cv	$$setvarz$$
8	5 7 6	co	$$class\left(y+z\right)$$
9	1	cv	$$setvarx$$
10	8 9	wceq	$$wffy+z=x$$
11	10 4 2	crio	$$class\left(\iota z\in ℝ|y+z=x\right)$$
12	1 3 2 2 11	cmpo	$$class\left(x\in ℝ,y\in ℝ⟼\left(\iota z\in ℝ|y+z=x\right)\right)$$
13	0 12	wceq	$$wff{-}_{ℝ}=\left(x\in ℝ,y\in ℝ⟼\left(\iota z\in ℝ|y+z=x\right)\right)$$