Definition df-refld 21646

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 21645	. 2 class ℝfld
2		ccnfld 21387	. . 3 class ℂfld
3		cr 11183	. . 3 class ℝ
4		cress 17287	. . 3 class ↾s
5	2, 3, 4	co 7448	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1537	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  21647  remulg  21648  resubdrg  21649  resubgval  21650  replusg  21651  remulr  21652  re0g  21653  re1r  21654  rele2  21655  relt  21656  reds  21657  redvr  21658  retos  21659  refld  21660  refldcj  21661  regsumsupp  21663  rzgrp  21664  tgioo3  24846  recvs  25198  recvsOLD  25199  retopn  25432  recms  25433  reust  25434  rrxcph  25445  rrxdsfi  25464  reefgim  26512  amgmlem  27051  nn0omnd  33338  nn0archi  33340  xrge0slmod  33341  ccfldextrr  33661  ccfldsrarelvec  33681  ccfldextdgrr  33682  rezh  33917  rrhcn  33943  rerrext  33955  cnrrext  33956  qqtopn  33957  bj-rveccmod  37268  amgmwlem  48896