Definition df-refld 21521

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 21520	. 2 class ℝfld
2		ccnfld 21271	. . 3 class ℂfld
3		cr 11074	. . 3 class ℝ
4		cress 17207	. . 3 class ↾s
5	2, 3, 4	co 7390	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1540	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  21522  remulg  21523  resubdrg  21524  resubgval  21525  replusg  21526  remulr  21527  re0g  21528  re1r  21529  rele2  21530  relt  21531  reds  21532  redvr  21533  retos  21534  refld  21535  refldcj  21536  regsumsupp  21538  rzgrp  21539  tgioo3  24701  recvs  25053  retopn  25286  recms  25287  reust  25288  rrxcph  25299  rrxdsfi  25318  reefgim  26367  amgmlem  26907  nn0omnd  33323  nn0archi  33325  xrge0slmod  33326  ccfldextrr  33649  ccfldsrarelvec  33673  ccfldextdgrr  33674  rezh  33966  rrhcn  33994  rerrext  34006  cnrrext  34007  qqtopn  34008  bj-rveccmod  37297  amgmwlem  49795