Definition df-refld 20751

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 20750	. 2 class ℝfld
2		ccnfld 20547	. . 3 class ℂfld
3		cr 10538	. . 3 class ℝ
4		cress 16486	. . 3 class ↾s
5	2, 3, 4	co 7158	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1537	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  20752  remulg  20753  resubdrg  20754  resubgval  20755  replusg  20756  remulr  20757  re0g  20758  re1r  20759  rele2  20760  relt  20761  reds  20762  redvr  20763  retos  20764  refld  20765  refldcj  20766  regsumsupp  20768  rzgrp  20769  tgioo3  23415  recvs  23752  retopn  23984  recms  23985  reust  23986  rrxcph  23997  rrxdsfi  24016  reefgim  25040  amgmlem  25569  nn0omnd  30916  nn0archi  30918  xrge0slmod  30919  ccfldextrr  31040  ccfldsrarelvec  31058  ccfldextdgrr  31059  rezh  31214  rrhcn  31240  rerrext  31252  cnrrext  31253  qqtopn  31254  bj-rveccmod  34585  amgmwlem  44910