Definition df-bj-onehalf 33629

Description: Define temporarily the real number "one-half". (Contributed by BJ, 4-Feb-2023.) Once the machinery is developed, the number "one-half" can be denoted by (1 / 2). (New usage is discouraged.)

Assertion

Ref	Expression
df-bj-onehalf	⊢ 1/2 = ⟨(℩𝑥 ∈ R (𝑥 +R 𝑥) = 1R), 0R⟩

Detailed syntax breakdown of Definition df-bj-onehalf

Step	Hyp	Ref	Expression
1		chalf 33628	. 2 class 1/2
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1655	. . . . . 6 class 𝑥
4		cplr 10013	. . . . . 6 class +R
5	3, 3, 4	co 6910	. . . . 5 class (𝑥 +R 𝑥)
6		c1r 10011	. . . . 5 class 1R
7	5, 6	wceq 1656	. . . 4 wff (𝑥 +R 𝑥) = 1R
8		cnr 10009	. . . 4 class R
9	7, 2, 8	crio 6870	. . 3 class (℩𝑥 ∈ R (𝑥 +R 𝑥) = 1R)
10		c0r 10010	. . 3 class 0R
11	9, 10	cop 4405	. 2 class ⟨(℩𝑥 ∈ R (𝑥 +R 𝑥) = 1R), 0R⟩
12	1, 11	wceq 1656	1 wff 1/2 = ⟨(℩𝑥 ∈ R (𝑥 +R 𝑥) = 1R), 0R⟩

This definition is referenced by: (None)