Definition df-refld 21377

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 21376	. 2 class ℝfld
2		ccnfld 21144	. . 3 class ℂfld
3		cr 11111	. . 3 class ℝ
4		cress 17177	. . 3 class ↾s
5	2, 3, 4	co 7411	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1539	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  21378  remulg  21379  resubdrg  21380  resubgval  21381  replusg  21382  remulr  21383  re0g  21384  re1r  21385  rele2  21386  relt  21387  reds  21388  redvr  21389  retos  21390  refld  21391  refldcj  21392  regsumsupp  21394  rzgrp  21395  tgioo3  24541  recvs  24893  recvsOLD  24894  retopn  25127  recms  25128  reust  25129  rrxcph  25140  rrxdsfi  25159  reefgim  26198  amgmlem  26730  nn0omnd  32730  nn0archi  32732  xrge0slmod  32733  ccfldextrr  33015  ccfldsrarelvec  33034  ccfldextdgrr  33035  rezh  33249  rrhcn  33275  rerrext  33287  cnrrext  33288  qqtopn  33289  bj-rveccmod  36486  amgmwlem  47936