Definition df-refld 21891

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 21890	. 2 class ℝfld
2		ccnfld 21658	. . 3 class ℂfld
3		cr 11180	. . 3 class ℝ
4		cress 17388	. . 3 class ↾s
5	2, 3, 4	co 7412	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1570	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is used by:  rebase  21892  remulg  21893  resubdrg  21894  resubgval  21895  replusg  21896  remulr  21897  re0g  21898  re1r  21899  rele2  21900  relt  21901  reds  21902  redvr  21903  retos  21904  refld  21905  refldcj  21906  regsumsupp  21908  rzgrp  21909  tgioo3  25105  recvs  25447  retopn  25680  recms  25681  reust  25682  rrxcph  25693  rrxdsfi  25712  reefgim  26759  amgmlem  27299  nn0omnd  33887  nn0archi  33890  xrge0slmod  33891  ccfldextrr  34260  ccfldsrarelvec  34285  ccfldextdgrr  34286  rezh  34583  rrhcn  34611  rerrext  34623  cnrrext  34624  qqtopn  34625  bj-rveccmod  38191  crosspdotsumlem  50908  amgmwlem  50931