Definition df-resub 41240

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

Assertion

Ref	Expression
df-resub	⊢ −ℝ = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (℩𝑧 ∈ ℝ (𝑦 + 𝑧) = 𝑥))

Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-resub

Step	Hyp	Ref	Expression
1		cresub 41239	. 2 class −ℝ
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cr 11108	. . 3 class ℝ
5	3	cv 1540	. . . . . 6 class 𝑦
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1540	. . . . . 6 class 𝑧
8		caddc 11112	. . . . . 6 class +
9	5, 7, 8	co 7408	. . . . 5 class (𝑦 + 𝑧)
10	2	cv 1540	. . . . 5 class 𝑥
11	9, 10	wceq 1541	. . . 4 wff (𝑦 + 𝑧) = 𝑥
12	11, 6, 4	crio 7363	. . 3 class (℩𝑧 ∈ ℝ (𝑦 + 𝑧) = 𝑥)
13	2, 3, 4, 4, 12	cmpo 7410	. 2 class (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (℩𝑧 ∈ ℝ (𝑦 + 𝑧) = 𝑥))
14	1, 13	wceq 1541	1 wff −ℝ = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (℩𝑧 ∈ ℝ (𝑦 + 𝑧) = 𝑥))

This definition is referenced by:  resubval  41241  resubf  41255