Definition df-refld 19951

Description: The field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.)

Assertion

Ref	Expression
df-refld	|- RRfld = (ℂfld ↾s RR )

Detailed syntax breakdown of Definition df-refld

Step	Hyp	Ref	Expression
1		crefld 19950	. 2 class RRfld
2		ccnfld 19746	. . 3 class ℂfld
3		cr 9935	. . 3 class RR
4		cress 15858	. . 3 class ↾s
5	2, 3, 4	co 6650	. 2 class (ℂfld ↾s RR )
6	1, 5	wceq 1483	1 wff RRfld = (ℂfld ↾s RR )

This definition is referenced by:  rebase  19952  remulg  19953  resubdrg  19954  resubgval  19955  replusg  19956  remulr  19957  re0g  19958  re1r  19959  rele2  19960  relt  19961  reds  19962  redvr  19963  retos  19964  refld  19965  refldcj  19966  regsumsupp  19968  tgioo3  22608  recvs  22946  retopn  23167  recms  23168  reust  23169  rrxcph  23180  reefgim  24204  rzgrp  24300  amgmlem  24716  nn0omnd  29841  nn0archi  29843  xrge0slmod  29844  rezh  30015  rrhcn  30041  rerrext  30053  cnrrext  30054  qqtopn  30055  rrxdsfi  40505  amgmwlem  42548