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

Definition df-refld 18619
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 18618 . 2  class RRfld
2 ccnfld 18399 . . 3  classfld
3 cr 9494 . . 3  class  RR
4 cress 14615 . . 3  classs
52, 3, 4co 6281 . 2  class  (flds  RR )
61, 5wceq 1383 1  wff RRfld  =  (flds  RR )
Colors of variables: wff setvar class
This definition is referenced by:  rebase  18620  remulg  18621  resubdrg  18622  resubgval  18623  replusg  18624  remulr  18625  re0g  18626  re1r  18627  rele2  18628  relt  18629  reds  18630  redvr  18631  retos  18632  refld  18633  refldcj  18634  regsumsupp  18636  tgioo3  21288  retopn  21789  recms  21790  reust  21791  rrxcph  21802  reefgim  22823  rzgrp  22919  amgmlem  23297  nn0omnd  27809  nn0archi  27811  xrge0slmod  27812  rezh  27930  rrhcn  27956  rerrext  27968  cnrrext  27969
  Copyright terms: Public domain W3C validator