Definition df-refld 21554

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 21553	. 2 class ℝfld
2		ccnfld 21296	. . 3 class ℂfld
3		cr 11139	. . 3 class ℝ
4		cress 17212	. . 3 class ↾s
5	2, 3, 4	co 7419	. 2 class (ℂfld ↾s ℝ)
6	1, 5	wceq 1533	1 wff ℝfld = (ℂfld ↾s ℝ)

This definition is referenced by:  rebase  21555  remulg  21556  resubdrg  21557  resubgval  21558  replusg  21559  remulr  21560  re0g  21561  re1r  21562  rele2  21563  relt  21564  reds  21565  redvr  21566  retos  21567  refld  21568  refldcj  21569  regsumsupp  21571  rzgrp  21572  tgioo3  24765  recvs  25117  recvsOLD  25118  retopn  25351  recms  25352  reust  25353  rrxcph  25364  rrxdsfi  25383  reefgim  26432  amgmlem  26967  nn0omnd  33156  nn0archi  33158  xrge0slmod  33159  ccfldextrr  33471  ccfldsrarelvec  33490  ccfldextdgrr  33491  rezh  33703  rrhcn  33729  rerrext  33741  cnrrext  33742  qqtopn  33743  bj-rveccmod  36912  amgmwlem  48421