Definition df-refld 21544

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 21543	. 2 class ℝfld
2		ccnfld 21293	. . 3 class ℂfld
3		cr 11012	. . 3 class ℝ
4		cress 17143	. . 3 class ↾s
5	2, 3, 4	co 7352	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1541	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  21545  remulg  21546  resubdrg  21547  resubgval  21548  replusg  21549  remulr  21550  re0g  21551  re1r  21552  rele2  21553  relt  21554  reds  21555  redvr  21556  retos  21557  refld  21558  refldcj  21559  regsumsupp  21561  rzgrp  21562  tgioo3  24722  recvs  25074  retopn  25307  recms  25308  reust  25309  rrxcph  25320  rrxdsfi  25339  reefgim  26388  amgmlem  26928  nn0omnd  33316  nn0archi  33319  xrge0slmod  33320  ccfldextrr  33680  ccfldsrarelvec  33705  ccfldextdgrr  33706  rezh  34003  rrhcn  34031  rerrext  34043  cnrrext  34044  qqtopn  34045  bj-rveccmod  37367  amgmwlem  49927