MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-refld Structured version   Unicode version

Definition df-refld 19172
Description: The field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.)
Assertion
Ref Expression
df-refld  |- RRfld  =  (flds  RR )

Detailed syntax breakdown of Definition df-refld
StepHypRef Expression
1 crefld 19171 . 2  class RRfld
2 ccnfld 18970 . . 3  classfld
3 cr 9546 . . 3  class  RR
4 cress 15122 . . 3  classs
52, 3, 4co 6306 . 2  class  (flds  RR )
61, 5wceq 1437 1  wff RRfld  =  (flds  RR )
Colors of variables: wff setvar class
This definition is referenced by:  rebase  19173  remulg  19174  resubdrg  19175  resubgval  19176  replusg  19177  remulr  19178  re0g  19179  re1r  19180  rele2  19181  relt  19182  reds  19183  redvr  19184  retos  19185  refld  19186  refldcj  19187  regsumsupp  19189  tgioo3  21822  retopn  22337  recms  22338  reust  22339  rrxcph  22350  reefgim  23404  rzgrp  23502  amgmlem  23914  nn0omnd  28613  nn0archi  28615  xrge0slmod  28616  rezh  28784  rrhcn  28810  rerrext  28822  cnrrext  28823  qqtopn  28824
  Copyright terms: Public domain W3C validator