Definition df-refld 20168

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 20167	. 2 class ℝfld
2		ccnfld 19961	. . 3 class ℂfld
3		cr 10141	. . 3 class ℝ
4		cress 16065	. . 3 class ↾s
5	2, 3, 4	co 6796	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1631	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  20169  remulg  20170  resubdrg  20171  resubgval  20172  replusg  20173  remulr  20174  re0g  20175  re1r  20176  rele2  20177  relt  20178  reds  20179  redvr  20180  retos  20181  refld  20182  refldcj  20183  regsumsupp  20185  tgioo3  22828  recvs  23165  retopn  23386  recms  23387  reust  23388  rrxcph  23399  reefgim  24424  rzgrp  24521  amgmlem  24937  nn0omnd  30181  nn0archi  30183  xrge0slmod  30184  rezh  30355  rrhcn  30381  rerrext  30393  cnrrext  30394  qqtopn  30395  rrxdsfi  41019  amgmwlem  43076