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

Definition df-refld 19222
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 19221 . 2  class RRfld
2 ccnfld 19019 . . 3  classfld
3 cr 9564 . . 3  class  RR
4 cress 15171 . . 3  classs
52, 3, 4co 6315 . 2  class  (flds  RR )
61, 5wceq 1455 1  wff RRfld  =  (flds  RR )
Colors of variables: wff setvar class
This definition is referenced by:  rebase  19223  remulg  19224  resubdrg  19225  resubgval  19226  replusg  19227  remulr  19228  re0g  19229  re1r  19230  rele2  19231  relt  19232  reds  19233  redvr  19234  retos  19235  refld  19236  refldcj  19237  regsumsupp  19239  tgioo3  21872  retopn  22387  recms  22388  reust  22389  rrxcph  22400  reefgim  23454  rzgrp  23552  amgmlem  23964  nn0omnd  28653  nn0archi  28655  xrge0slmod  28656  rezh  28824  rrhcn  28850  rerrext  28862  cnrrext  28863  qqtopn  28864  rrxdsfi  38192
  Copyright terms: Public domain W3C validator