Definition df-refld 20819

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 20818	. 2 class ℝfld
2		ccnfld 20606	. . 3 class ℂfld
3		cr 10879	. . 3 class ℝ
4		cress 16950	. . 3 class ↾s
5	2, 3, 4	co 7284	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1539	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  20820  remulg  20821  resubdrg  20822  resubgval  20823  replusg  20824  remulr  20825  re0g  20826  re1r  20827  rele2  20828  relt  20829  reds  20830  redvr  20831  retos  20832  refld  20833  refldcj  20834  regsumsupp  20836  rzgrp  20837  tgioo3  23977  recvs  24318  recvsOLD  24319  retopn  24552  recms  24553  reust  24554  rrxcph  24565  rrxdsfi  24584  reefgim  25618  amgmlem  26148  nn0omnd  31554  nn0archi  31556  xrge0slmod  31557  ccfldextrr  31732  ccfldsrarelvec  31750  ccfldextdgrr  31751  rezh  31930  rrhcn  31956  rerrext  31968  cnrrext  31969  qqtopn  31970  bj-rveccmod  35482  amgmwlem  46517