Definition df-refld 21585

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 21584	. 2 class ℝfld
2		ccnfld 21352	. . 3 class ℂfld
3		cr 11037	. . 3 class ℝ
4		cress 17200	. . 3 class ↾s
5	2, 3, 4	co 7367	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1542	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  21586  remulg  21587  resubdrg  21588  resubgval  21589  replusg  21590  remulr  21591  re0g  21592  re1r  21593  rele2  21594  relt  21595  reds  21596  redvr  21597  retos  21598  refld  21599  refldcj  21600  regsumsupp  21602  rzgrp  21603  tgioo3  24771  recvs  25113  retopn  25346  recms  25347  reust  25348  rrxcph  25359  rrxdsfi  25378  reefgim  26415  amgmlem  26953  nn0omnd  33404  nn0archi  33407  xrge0slmod  33408  ccfldextrr  33790  ccfldsrarelvec  33815  ccfldextdgrr  33816  rezh  34113  rrhcn  34141  rerrext  34153  cnrrext  34154  qqtopn  34155  bj-rveccmod  37616  amgmwlem  50277