Definition df-refld 21824

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 21823	. 2 class ℝfld
2		ccnfld 21591	. . 3 class ℂfld
3		cr 11127	. . 3 class ℝ
4		cress 17328	. . 3 class ↾s
5	2, 3, 4	co 7417	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1570	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is used by:  rebase  21825  remulg  21826  resubdrg  21827  resubgval  21828  replusg  21829  remulr  21830  re0g  21831  re1r  21832  rele2  21833  relt  21834  reds  21835  redvr  21836  retos  21837  refld  21838  refldcj  21839  regsumsupp  21841  rzgrp  21842  tgioo3  25038  recvs  25380  retopn  25613  recms  25614  reust  25615  rrxcph  25626  rrxdsfi  25645  reefgim  26693  amgmlem  27234  nn0omnd  33792  nn0archi  33795  xrge0slmod  33796  ccfldextrr  34164  ccfldsrarelvec  34189  ccfldextdgrr  34190  rezh  34487  rrhcn  34515  rerrext  34527  cnrrext  34528  qqtopn  34529  bj-rveccmod  38062  crosspdotsumlem  50805  amgmwlem  50828