Definition df-refld 21736

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 21735	. 2 class ℝfld
2		ccnfld 21503	. . 3 class ℂfld
3		cr 11100	. . 3 class ℝ
4		cress 17291	. . 3 class ↾s
5	2, 3, 4	co 7412	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1570	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  21737  remulg  21738  resubdrg  21739  resubgval  21740  replusg  21741  remulr  21742  re0g  21743  re1r  21744  rele2  21745  relt  21746  reds  21747  redvr  21748  retos  21749  refld  21750  refldcj  21751  regsumsupp  21753  rzgrp  21754  tgioo3  24944  recvs  25286  retopn  25519  recms  25520  reust  25521  rrxcph  25532  rrxdsfi  25551  reefgim  26591  amgmlem  27132  nn0omnd  33642  nn0archi  33645  xrge0slmod  33646  ccfldextrr  34014  ccfldsrarelvec  34039  ccfldextdgrr  34040  rezh  34337  rrhcn  34365  rerrext  34377  cnrrext  34378  qqtopn  34379  bj-rveccmod  37924  amgmwlem  50579