Definition df-refld 20294

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 20293	. 2 class ℝfld
2		ccnfld 20091	. . 3 class ℂfld
3		cr 10525	. . 3 class ℝ
4		cress 16476	. . 3 class ↾s
5	2, 3, 4	co 7135	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1538	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  20295  remulg  20296  resubdrg  20297  resubgval  20298  replusg  20299  remulr  20300  re0g  20301  re1r  20302  rele2  20303  relt  20304  reds  20305  redvr  20306  retos  20307  refld  20308  refldcj  20309  regsumsupp  20311  rzgrp  20312  tgioo3  23410  recvs  23751  retopn  23983  recms  23984  reust  23985  rrxcph  23996  rrxdsfi  24015  reefgim  25045  amgmlem  25575  nn0omnd  30965  nn0archi  30967  xrge0slmod  30968  ccfldextrr  31126  ccfldsrarelvec  31144  ccfldextdgrr  31145  rezh  31322  rrhcn  31348  rerrext  31360  cnrrext  31361  qqtopn  31362  bj-rveccmod  34716  amgmwlem  45330