Definition df-refld 20312

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 20311	. 2 class ℝfld
2		ccnfld 20106	. . 3 class ℂfld
3		cr 10251	. . 3 class ℝ
4		cress 16223	. . 3 class ↾s
5	2, 3, 4	co 6905	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1656	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  20313  remulg  20314  resubdrg  20315  resubgval  20316  replusg  20317  remulr  20318  re0g  20319  re1r  20320  rele2  20321  relt  20322  reds  20323  redvr  20324  retos  20325  refld  20326  refldcj  20327  regsumsupp  20329  rzgrp  20330  tgioo3  22978  recvs  23315  retopn  23547  recms  23548  reust  23549  rrxcph  23560  rrxdsfi  23579  reefgim  24603  amgmlem  25129  nn0omnd  30375  nn0archi  30377  xrge0slmod  30378  rezh  30549  rrhcn  30575  rerrext  30587  cnrrext  30588  qqtopn  30589  amgmwlem  43437