Definition df-refld 21720

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 21719	. 2 class ℝfld
2		ccnfld 21487	. . 3 class ℂfld
3		cr 11095	. . 3 class ℝ
4		cress 17286	. . 3 class ↾s
5	2, 3, 4	co 7408	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1567	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  21721  remulg  21722  resubdrg  21723  resubgval  21724  replusg  21725  remulr  21726  re0g  21727  re1r  21728  rele2  21729  relt  21730  reds  21731  redvr  21732  retos  21733  refld  21734  refldcj  21735  regsumsupp  21737  rzgrp  21738  tgioo3  24928  recvs  25270  retopn  25503  recms  25504  reust  25505  rrxcph  25516  rrxdsfi  25535  reefgim  26575  amgmlem  27116  nn0omnd  33603  nn0archi  33606  xrge0slmod  33607  ccfldextrr  33977  ccfldsrarelvec  34002  ccfldextdgrr  34003  rezh  34300  rrhcn  34328  rerrext  34340  cnrrext  34341  qqtopn  34342  bj-rveccmod  37829  amgmwlem  50471