Definition df-refld 21587

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 21586	. 2 class ℝfld
2		ccnfld 21354	. . 3 class ℂfld
3		cr 11035	. . 3 class ℝ
4		cress 17198	. . 3 class ↾s
5	2, 3, 4	co 7363	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1547	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  21588  remulg  21589  resubdrg  21590  resubgval  21591  replusg  21592  remulr  21593  re0g  21594  re1r  21595  rele2  21596  relt  21597  reds  21598  redvr  21599  retos  21600  refld  21601  refldcj  21602  regsumsupp  21604  rzgrp  21605  tgioo3  24796  recvs  25138  retopn  25371  recms  25372  reust  25373  rrxcph  25384  rrxdsfi  25403  reefgim  26440  amgmlem  26978  nn0omnd  33434  nn0archi  33437  xrge0slmod  33438  ccfldextrr  33837  ccfldsrarelvec  33862  ccfldextdgrr  33863  rezh  34160  rrhcn  34188  rerrext  34200  cnrrext  34201  qqtopn  34202  bj-rveccmod  37669  amgmwlem  50299