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

Definition df-refld 18408
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 18407 . 2  class RRfld
2 ccnfld 18191 . . 3  classfld
3 cr 9487 . . 3  class  RR
4 cress 14487 . . 3  classs
52, 3, 4co 6282 . 2  class  (flds  RR )
61, 5wceq 1379 1  wff RRfld  =  (flds  RR )
Colors of variables: wff setvar class
This definition is referenced by:  rebase  18409  remulg  18410  resubdrg  18411  resubgval  18412  replusg  18413  remulr  18414  re0g  18415  re1r  18416  rele2  18417  relt  18418  reds  18419  redvr  18420  retos  18421  refld  18422  refldcj  18423  regsumsupp  18425  tgioo3  21045  retopn  21546  recms  21547  reust  21548  rrxcph  21559  reefgim  22579  amgmlem  23047  nn0omnd  27494  nn0archi  27496  xrge0slmod  27497  rezh  27588  rrhcn  27614  rerrext  27626  cnrrext  27627
  Copyright terms: Public domain W3C validator