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 20748
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 20747 . 2 class fld
2 ccnfld 20544 . . 3 class fld
3 cr 10535 . . 3 class
4 cress 16483 . . 3 class s
52, 3, 4co 7155 . 2 class (ℂflds ℝ)
61, 5wceq 1533 1 wff fld = (ℂflds ℝ)
Colors of variables: wff setvar class
This definition is referenced by:  rebase  20749  remulg  20750  resubdrg  20751  resubgval  20752  replusg  20753  remulr  20754  re0g  20755  re1r  20756  rele2  20757  relt  20758  reds  20759  redvr  20760  retos  20761  refld  20762  refldcj  20763  regsumsupp  20765  rzgrp  20766  tgioo3  23412  recvs  23749  retopn  23981  recms  23982  reust  23983  rrxcph  23994  rrxdsfi  24013  reefgim  25037  amgmlem  25566  nn0omnd  30914  nn0archi  30916  xrge0slmod  30917  ccfldextrr  31038  ccfldsrarelvec  31056  ccfldextdgrr  31057  rezh  31212  rrhcn  31238  rerrext  31250  cnrrext  31251  qqtopn  31252  bj-rveccmod  34582  amgmwlem  44902
  Copyright terms: Public domain W3C validator