Definition df-refld 21540

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 21539	. 2 class ℝfld
2		ccnfld 21289	. . 3 class ℂfld
3		cr 11002	. . 3 class ℝ
4		cress 17138	. . 3 class ↾s
5	2, 3, 4	co 7346	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1541	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  21541  remulg  21542  resubdrg  21543  resubgval  21544  replusg  21545  remulr  21546  re0g  21547  re1r  21548  rele2  21549  relt  21550  reds  21551  redvr  21552  retos  21553  refld  21554  refldcj  21555  regsumsupp  21557  rzgrp  21558  tgioo3  24719  recvs  25071  retopn  25304  recms  25305  reust  25306  rrxcph  25317  rrxdsfi  25336  reefgim  26385  amgmlem  26925  nn0omnd  33304  nn0archi  33307  xrge0slmod  33308  ccfldextrr  33654  ccfldsrarelvec  33679  ccfldextdgrr  33680  rezh  33977  rrhcn  34005  rerrext  34017  cnrrext  34018  qqtopn  34019  bj-rveccmod  37335  amgmwlem  49833