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 19770
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 19769 . 2 class fld
2 ccnfld 19567 . . 3 class fld
3 cr 9814 . . 3 class
4 cress 15696 . . 3 class s
52, 3, 4co 6549 . 2 class (ℂflds ℝ)
61, 5wceq 1475 1 wff fld = (ℂflds ℝ)
Colors of variables: wff setvar class
This definition is referenced by:  rebase  19771  remulg  19772  resubdrg  19773  resubgval  19774  replusg  19775  remulr  19776  re0g  19777  re1r  19778  rele2  19779  relt  19780  reds  19781  redvr  19782  retos  19783  refld  19784  refldcj  19785  regsumsupp  19787  tgioo3  22416  recvs  22754  retopn  22975  recms  22976  reust  22977  rrxcph  22988  reefgim  24008  rzgrp  24104  amgmlem  24516  nn0omnd  29172  nn0archi  29174  xrge0slmod  29175  rezh  29343  rrhcn  29369  rerrext  29381  cnrrext  29382  qqtopn  29383  rrxdsfi  39181  amgmwlem  42357
  Copyright terms: Public domain W3C validator