Definition df-refld

Description: The field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019)

	Ref	Expression
Assertion	df-refld	$$⊢{ℝ}_{\mathrm{fld}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crefld	$$class{ℝ}_{\mathrm{fld}}$$
1		ccnfld	$$class{ℂ}_{\mathrm{fld}}$$
2		cress	$$class{\upharpoonright }_{𝑠}$$
3		cr	$$classℝ$$
4	1 3 2	co	$$class\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right)$$
5	0 4	wceq	$$wff{ℝ}_{\mathrm{fld}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ$$