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

Definition df-refld 20168
Description: The field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.)
Assertion
Ref Expression
df-refld fld = (ℂflds ℝ)

Detailed syntax breakdown of Definition df-refld
StepHypRef Expression
1 crefld 20167 . 2 class fld
2 ccnfld 19961 . . 3 class fld
3 cr 10141 . . 3 class
4 cress 16065 . . 3 class s
52, 3, 4co 6796 . 2 class (ℂflds ℝ)
61, 5wceq 1631 1 wff fld = (ℂflds ℝ)
Colors of variables: wff setvar class
This definition is referenced by:  rebase  20169  remulg  20170  resubdrg  20171  resubgval  20172  replusg  20173  remulr  20174  re0g  20175  re1r  20176  rele2  20177  relt  20178  reds  20179  redvr  20180  retos  20181  refld  20182  refldcj  20183  regsumsupp  20185  tgioo3  22828  recvs  23165  retopn  23386  recms  23387  reust  23388  rrxcph  23399  reefgim  24424  rzgrp  24521  amgmlem  24937  nn0omnd  30181  nn0archi  30183  xrge0slmod  30184  rezh  30355  rrhcn  30381  rerrext  30393  cnrrext  30394  qqtopn  30395  rrxdsfi  41019  amgmwlem  43076
  Copyright terms: Public domain W3C validator