Definition df-refld 21623

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 21622	. 2 class ℝfld
2		ccnfld 21364	. . 3 class ℂfld
3		cr 11154	. . 3 class ℝ
4		cress 17274	. . 3 class ↾s
5	2, 3, 4	co 7431	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1540	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  21624  remulg  21625  resubdrg  21626  resubgval  21627  replusg  21628  remulr  21629  re0g  21630  re1r  21631  rele2  21632  relt  21633  reds  21634  redvr  21635  retos  21636  refld  21637  refldcj  21638  regsumsupp  21640  rzgrp  21641  tgioo3  24827  recvs  25179  recvsOLD  25180  retopn  25413  recms  25414  reust  25415  rrxcph  25426  rrxdsfi  25445  reefgim  26494  amgmlem  27033  nn0omnd  33373  nn0archi  33375  xrge0slmod  33376  ccfldextrr  33699  ccfldsrarelvec  33721  ccfldextdgrr  33722  rezh  33970  rrhcn  33998  rerrext  34010  cnrrext  34011  qqtopn  34012  bj-rveccmod  37303  amgmwlem  49321