Definition df-refld 20722

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 20721	. 2 class ℝfld
2		ccnfld 20510	. . 3 class ℂfld
3		cr 10801	. . 3 class ℝ
4		cress 16867	. . 3 class ↾s
5	2, 3, 4	co 7255	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1539	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  20723  remulg  20724  resubdrg  20725  resubgval  20726  replusg  20727  remulr  20728  re0g  20729  re1r  20730  rele2  20731  relt  20732  reds  20733  redvr  20734  retos  20735  refld  20736  refldcj  20737  regsumsupp  20739  rzgrp  20740  tgioo3  23874  recvs  24215  retopn  24448  recms  24449  reust  24450  rrxcph  24461  rrxdsfi  24480  reefgim  25514  amgmlem  26044  nn0omnd  31447  nn0archi  31449  xrge0slmod  31450  ccfldextrr  31625  ccfldsrarelvec  31643  ccfldextdgrr  31644  rezh  31821  rrhcn  31847  rerrext  31859  cnrrext  31860  qqtopn  31861  bj-rveccmod  35400  amgmwlem  46392