Definition df-refld 21563

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 21562	. 2 class ℝfld
2		ccnfld 21313	. . 3 class ℂfld
3		cr 11126	. . 3 class ℝ
4		cress 17249	. . 3 class ↾s
5	2, 3, 4	co 7403	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1540	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  21564  remulg  21565  resubdrg  21566  resubgval  21567  replusg  21568  remulr  21569  re0g  21570  re1r  21571  rele2  21572  relt  21573  reds  21574  redvr  21575  retos  21576  refld  21577  refldcj  21578  regsumsupp  21580  rzgrp  21581  tgioo3  24743  recvs  25095  recvsOLD  25096  retopn  25329  recms  25330  reust  25331  rrxcph  25342  rrxdsfi  25361  reefgim  26410  amgmlem  26950  nn0omnd  33306  nn0archi  33308  xrge0slmod  33309  ccfldextrr  33634  ccfldsrarelvec  33658  ccfldextdgrr  33659  rezh  33946  rrhcn  33974  rerrext  33986  cnrrext  33987  qqtopn  33988  bj-rveccmod  37266  amgmwlem  49614