Definition df-refld 21715

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 21714	. 2 class ℝfld
2		ccnfld 21482	. . 3 class ℂfld
3		cr 11087	. . 3 class ℝ
4		cress 17280	. . 3 class ↾s
5	2, 3, 4	co 7400	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1563	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  21716  remulg  21717  resubdrg  21718  resubgval  21719  replusg  21720  remulr  21721  re0g  21722  re1r  21723  rele2  21724  relt  21725  reds  21726  redvr  21727  retos  21728  refld  21729  refldcj  21730  regsumsupp  21732  rzgrp  21733  tgioo3  24924  recvs  25266  retopn  25499  recms  25500  reust  25501  rrxcph  25512  rrxdsfi  25531  reefgim  26571  amgmlem  27112  nn0omnd  33579  nn0archi  33582  xrge0slmod  33583  ccfldextrr  33953  ccfldsrarelvec  33978  ccfldextdgrr  33979  rezh  34276  rrhcn  34304  rerrext  34316  cnrrext  34317  qqtopn  34318  bj-rveccmod  37806  amgmwlem  50431