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 19932
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 19931 . 2 class fld
2 ccnfld 19727 . . 3 class fld
3 cr 9920 . . 3 class
4 cress 15839 . . 3 class s
52, 3, 4co 6635 . 2 class (ℂflds ℝ)
61, 5wceq 1481 1 wff fld = (ℂflds ℝ)
Colors of variables: wff setvar class
This definition is referenced by:  rebase  19933  remulg  19934  resubdrg  19935  resubgval  19936  replusg  19937  remulr  19938  re0g  19939  re1r  19940  rele2  19941  relt  19942  reds  19943  redvr  19944  retos  19945  refld  19946  refldcj  19947  regsumsupp  19949  tgioo3  22589  recvs  22927  retopn  23148  recms  23149  reust  23150  rrxcph  23161  reefgim  24185  rzgrp  24281  amgmlem  24697  nn0omnd  29815  nn0archi  29817  xrge0slmod  29818  rezh  29989  rrhcn  30015  rerrext  30027  cnrrext  30028  qqtopn  30029  rrxdsfi  40268  amgmwlem  42313
  Copyright terms: Public domain W3C validator