Definition df-refld 20808

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 20807	. 2 class ℝfld
2		ccnfld 20595	. . 3 class ℂfld
3		cr 10871	. . 3 class ℝ
4		cress 16939	. . 3 class ↾s
5	2, 3, 4	co 7271	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1542	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  20809  remulg  20810  resubdrg  20811  resubgval  20812  replusg  20813  remulr  20814  re0g  20815  re1r  20816  rele2  20817  relt  20818  reds  20819  redvr  20820  retos  20821  refld  20822  refldcj  20823  regsumsupp  20825  rzgrp  20826  tgioo3  23966  recvs  24307  recvsOLD  24308  retopn  24541  recms  24542  reust  24543  rrxcph  24554  rrxdsfi  24573  reefgim  25607  amgmlem  26137  nn0omnd  31541  nn0archi  31543  xrge0slmod  31544  ccfldextrr  31719  ccfldsrarelvec  31737  ccfldextdgrr  31738  rezh  31917  rrhcn  31943  rerrext  31955  cnrrext  31956  qqtopn  31957  bj-rveccmod  35469  amgmwlem  46475