Definition df-refld 20741

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 20740	. 2 class ℝfld
2		ccnfld 20537	. . 3 class ℂfld
3		cr 10528	. . 3 class ℝ
4		cress 16476	. . 3 class ↾s
5	2, 3, 4	co 7148	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1531	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  20742  remulg  20743  resubdrg  20744  resubgval  20745  replusg  20746  remulr  20747  re0g  20748  re1r  20749  rele2  20750  relt  20751  reds  20752  redvr  20753  retos  20754  refld  20755  refldcj  20756  regsumsupp  20758  rzgrp  20759  tgioo3  23405  recvs  23742  retopn  23974  recms  23975  reust  23976  rrxcph  23987  rrxdsfi  24006  reefgim  25030  amgmlem  25559  nn0omnd  30907  nn0archi  30909  xrge0slmod  30910  ccfldextrr  31031  ccfldsrarelvec  31049  ccfldextdgrr  31050  rezh  31205  rrhcn  31231  rerrext  31243  cnrrext  31244  qqtopn  31245  bj-rveccmod  34575  amgmwlem  44893