Definition df-refld 21640

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 21639	. 2 class ℝfld
2		ccnfld 21381	. . 3 class ℂfld
3		cr 11151	. . 3 class ℝ
4		cress 17273	. . 3 class ↾s
5	2, 3, 4	co 7430	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1536	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  21641  remulg  21642  resubdrg  21643  resubgval  21644  replusg  21645  remulr  21646  re0g  21647  re1r  21648  rele2  21649  relt  21650  reds  21651  redvr  21652  retos  21653  refld  21654  refldcj  21655  regsumsupp  21657  rzgrp  21658  tgioo3  24840  recvs  25192  recvsOLD  25193  retopn  25426  recms  25427  reust  25428  rrxcph  25439  rrxdsfi  25458  reefgim  26508  amgmlem  27047  nn0omnd  33352  nn0archi  33354  xrge0slmod  33355  ccfldextrr  33675  ccfldsrarelvec  33695  ccfldextdgrr  33696  rezh  33931  rrhcn  33959  rerrext  33971  cnrrext  33972  qqtopn  33973  bj-rveccmod  37284  amgmwlem  49032