Definition df-refld 21572

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

This definition is referenced by:  rebase  21573  remulg  21574  resubdrg  21575  resubgval  21576  replusg  21577  remulr  21578  re0g  21579  re1r  21580  rele2  21581  relt  21582  reds  21583  redvr  21584  retos  21585  refld  21586  refldcj  21587  regsumsupp  21589  rzgrp  21590  tgioo3  24762  recvs  25114  retopn  25347  recms  25348  reust  25349  rrxcph  25360  rrxdsfi  25379  reefgim  26428  amgmlem  26968  nn0omnd  33436  nn0archi  33439  xrge0slmod  33440  ccfldextrr  33823  ccfldsrarelvec  33848  ccfldextdgrr  33849  rezh  34146  rrhcn  34174  rerrext  34186  cnrrext  34187  qqtopn  34188  bj-rveccmod  37551  amgmwlem  50155