Definition df-refld 21637

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 21636	. 2 class ℝfld
2		ccnfld 21404	. . 3 class ℂfld
3		cr 11069	. . 3 class ℝ
4		cress 17249	. . 3 class ↾s
5	2, 3, 4	co 7392	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1559	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  21638  remulg  21639  resubdrg  21640  resubgval  21641  replusg  21642  remulr  21643  re0g  21644  re1r  21645  rele2  21646  relt  21647  reds  21648  redvr  21649  retos  21650  refld  21651  refldcj  21652  regsumsupp  21654  rzgrp  21655  tgioo3  24846  recvs  25188  retopn  25421  recms  25422  reust  25423  rrxcph  25434  rrxdsfi  25453  reefgim  26490  amgmlem  27031  nn0omnd  33491  nn0archi  33494  xrge0slmod  33495  ccfldextrr  33904  ccfldsrarelvec  33929  ccfldextdgrr  33930  rezh  34227  rrhcn  34255  rerrext  34267  cnrrext  34268  qqtopn  34269  bj-rveccmod  37758  amgmwlem  50387