Definition df-refld 21149

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 21148	. 2 class ℝfld
2		ccnfld 20936	. . 3 class ℂfld
3		cr 11105	. . 3 class ℝ
4		cress 17169	. . 3 class ↾s
5	2, 3, 4	co 7405	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1541	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  21150  remulg  21151  resubdrg  21152  resubgval  21153  replusg  21154  remulr  21155  re0g  21156  re1r  21157  rele2  21158  relt  21159  reds  21160  redvr  21161  retos  21162  refld  21163  refldcj  21164  regsumsupp  21166  rzgrp  21167  tgioo3  24312  recvs  24653  recvsOLD  24654  retopn  24887  recms  24888  reust  24889  rrxcph  24900  rrxdsfi  24919  reefgim  25953  amgmlem  26483  nn0omnd  32448  nn0archi  32450  xrge0slmod  32451  ccfldextrr  32715  ccfldsrarelvec  32733  ccfldextdgrr  32734  rezh  32939  rrhcn  32965  rerrext  32977  cnrrext  32978  qqtopn  32979  bj-rveccmod  36171  amgmwlem  47802