Definition df-refld 21560

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 21559	. 2 class ℝfld
2		ccnfld 21309	. . 3 class ℂfld
3		cr 11025	. . 3 class ℝ
4		cress 17157	. . 3 class ↾s
5	2, 3, 4	co 7358	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1541	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  21561  remulg  21562  resubdrg  21563  resubgval  21564  replusg  21565  remulr  21566  re0g  21567  re1r  21568  rele2  21569  relt  21570  reds  21571  redvr  21572  retos  21573  refld  21574  refldcj  21575  regsumsupp  21577  rzgrp  21578  tgioo3  24750  recvs  25102  retopn  25335  recms  25336  reust  25337  rrxcph  25348  rrxdsfi  25367  reefgim  26416  amgmlem  26956  nn0omnd  33425  nn0archi  33428  xrge0slmod  33429  ccfldextrr  33803  ccfldsrarelvec  33828  ccfldextdgrr  33829  rezh  34126  rrhcn  34154  rerrext  34166  cnrrext  34167  qqtopn  34168  bj-rveccmod  37503  amgmwlem  50043