Definition df-refld 21941

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

Assertion

Ref	Expression
df-refld	⊢ ℝfld = (ℂfld ↾s ℝ)

Detailed syntax breakdown of Definition df-refld

Step	Hyp	Ref	Expression
1		crefld 21940	. 2 class ℝfld
2		ccnfld 21708	. . 3 class ℂfld
3		cr 11226	. . 3 class ℝ
4		cress 17437	. . 3 class ↾s
5	2, 3, 4	co 7443	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1570	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is used by:  rebase  21942  remulg  21943  resubdrg  21944  resubgval  21945  replusg  21946  remulr  21947  re0g  21948  re1r  21949  rele2  21950  relt  21951  reds  21952  redvr  21953  retos  21954  refld  21955  refldcj  21956  regsumsupp  21958  rzgrp  21959  tgioo3  25155  recvs  25497  retopn  25730  recms  25731  reust  25732  rrxcph  25743  rrxdsfi  25762  reefgim  26807  amgmlem  27347  nn0omnd  33975  nn0archi  33978  xrge0slmod  33979  ccfldextrr  34348  ccfldsrarelvec  34373  ccfldextdgrr  34374  rezh  34671  rrhcn  34699  rerrext  34711  cnrrext  34712  qqtopn  34713  bj-rveccmod  38415  crosspdotsumlem  51244  amgmwlem  51267