Definition df-refld 21514

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 21513	. 2 class ℝfld
2		ccnfld 21264	. . 3 class ℂfld
3		cr 11067	. . 3 class ℝ
4		cress 17200	. . 3 class ↾s
5	2, 3, 4	co 7387	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1540	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  21515  remulg  21516  resubdrg  21517  resubgval  21518  replusg  21519  remulr  21520  re0g  21521  re1r  21522  rele2  21523  relt  21524  reds  21525  redvr  21526  retos  21527  refld  21528  refldcj  21529  regsumsupp  21531  rzgrp  21532  tgioo3  24694  recvs  25046  retopn  25279  recms  25280  reust  25281  rrxcph  25292  rrxdsfi  25311  reefgim  26360  amgmlem  26900  nn0omnd  33316  nn0archi  33318  xrge0slmod  33319  ccfldextrr  33642  ccfldsrarelvec  33666  ccfldextdgrr  33667  rezh  33959  rrhcn  33987  rerrext  33999  cnrrext  34000  qqtopn  34001  bj-rveccmod  37290  amgmwlem  49791