Definition df-refld 21530

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 21529	. 2 class ℝfld
2		ccnfld 21279	. . 3 class ℂfld
3		cr 11027	. . 3 class ℝ
4		cress 17159	. . 3 class ↾s
5	2, 3, 4	co 7353	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1540	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  21531  remulg  21532  resubdrg  21533  resubgval  21534  replusg  21535  remulr  21536  re0g  21537  re1r  21538  rele2  21539  relt  21540  reds  21541  redvr  21542  retos  21543  refld  21544  refldcj  21545  regsumsupp  21547  rzgrp  21548  tgioo3  24710  recvs  25062  retopn  25295  recms  25296  reust  25297  rrxcph  25308  rrxdsfi  25327  reefgim  26376  amgmlem  26916  nn0omnd  33292  nn0archi  33294  xrge0slmod  33295  ccfldextrr  33618  ccfldsrarelvec  33642  ccfldextdgrr  33643  rezh  33935  rrhcn  33963  rerrext  33975  cnrrext  33976  qqtopn  33977  bj-rveccmod  37275  amgmwlem  49788