Definition df-refld 21378

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 21377	. 2 class ℝfld
2		ccnfld 21145	. . 3 class ℂfld
3		cr 11112	. . 3 class ℝ
4		cress 17178	. . 3 class ↾s
5	2, 3, 4	co 7412	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1540	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  21379  remulg  21380  resubdrg  21381  resubgval  21382  replusg  21383  remulr  21384  re0g  21385  re1r  21386  rele2  21387  relt  21388  reds  21389  redvr  21390  retos  21391  refld  21392  refldcj  21393  regsumsupp  21395  rzgrp  21396  tgioo3  24542  recvs  24894  recvsOLD  24895  retopn  25128  recms  25129  reust  25130  rrxcph  25141  rrxdsfi  25160  reefgim  26195  amgmlem  26727  nn0omnd  32727  nn0archi  32729  xrge0slmod  32730  ccfldextrr  33012  ccfldsrarelvec  33031  ccfldextdgrr  33032  rezh  33246  rrhcn  33272  rerrext  33284  cnrrext  33285  qqtopn  33286  bj-rveccmod  36487  amgmwlem  47938