Definition df-refld 21595

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 21594	. 2 class ℝfld
2		ccnfld 21344	. . 3 class ℂfld
3		cr 11028	. . 3 class ℝ
4		cress 17191	. . 3 class ↾s
5	2, 3, 4	co 7360	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1542	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  21596  remulg  21597  resubdrg  21598  resubgval  21599  replusg  21600  remulr  21601  re0g  21602  re1r  21603  rele2  21604  relt  21605  reds  21606  redvr  21607  retos  21608  refld  21609  refldcj  21610  regsumsupp  21612  rzgrp  21613  tgioo3  24781  recvs  25123  retopn  25356  recms  25357  reust  25358  rrxcph  25369  rrxdsfi  25388  reefgim  26428  amgmlem  26967  nn0omnd  33419  nn0archi  33422  xrge0slmod  33423  ccfldextrr  33806  ccfldsrarelvec  33831  ccfldextdgrr  33832  rezh  34129  rrhcn  34157  rerrext  34169  cnrrext  34170  qqtopn  34171  bj-rveccmod  37632  amgmwlem  50289