Definition df-refld 21792

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 21791	. 2 class ℝfld
2		ccnfld 21559	. . 3 class ℂfld
3		cr 11117	. . 3 class ℝ
4		cress 17315	. . 3 class ↾s
5	2, 3, 4	co 7423	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1570	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is used by:  rebase  21793  remulg  21794  resubdrg  21795  resubgval  21796  replusg  21797  remulr  21798  re0g  21799  re1r  21800  rele2  21801  relt  21802  reds  21803  redvr  21804  retos  21805  refld  21806  refldcj  21807  regsumsupp  21809  rzgrp  21810  tgioo3  25000  recvs  25342  retopn  25575  recms  25576  reust  25577  rrxcph  25588  rrxdsfi  25607  reefgim  26650  amgmlem  27191  nn0omnd  33695  nn0archi  33698  xrge0slmod  33699  ccfldextrr  34067  ccfldsrarelvec  34092  ccfldextdgrr  34093  rezh  34390  rrhcn  34418  rerrext  34430  cnrrext  34431  qqtopn  34432  bj-rveccmod  37987  crosspdotsumi  50687  amgmwlem  50691