Definition df-refld 21916

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 21915	. 2 class ℝfld
2		ccnfld 21683	. . 3 class ℂfld
3		cr 11202	. . 3 class ℝ
4		cress 17413	. . 3 class ↾s
5	2, 3, 4	co 7420	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1569	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is used by:  rebase  21917  remulg  21918  resubdrg  21919  resubgval  21920  replusg  21921  remulr  21922  re0g  21923  re1r  21924  rele2  21925  relt  21926  reds  21927  redvr  21928  retos  21929  refld  21930  refldcj  21931  regsumsupp  21933  rzgrp  21934  tgioo3  25130  recvs  25472  retopn  25705  recms  25706  reust  25707  rrxcph  25718  rrxdsfi  25737  reefgim  26782  amgmlem  27322  nn0omnd  33951  nn0archi  33954  xrge0slmod  33955  ccfldextrr  34324  ccfldsrarelvec  34349  ccfldextdgrr  34350  rezh  34647  rrhcn  34675  rerrext  34687  cnrrext  34688  qqtopn  34689  bj-rveccmod  38316  crosspdotsumlem  51132  amgmwlem  51155