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 21554
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 21553 . 2 class fld
2 ccnfld 21296 . . 3 class fld
3 cr 11139 . . 3 class
4 cress 17212 . . 3 class s
52, 3, 4co 7419 . 2 class (ℂflds ℝ)
61, 5wceq 1533 1 wff fld = (ℂflds ℝ)
Colors of variables: wff setvar class
This definition is referenced by:  rebase  21555  remulg  21556  resubdrg  21557  resubgval  21558  replusg  21559  remulr  21560  re0g  21561  re1r  21562  rele2  21563  relt  21564  reds  21565  redvr  21566  retos  21567  refld  21568  refldcj  21569  regsumsupp  21571  rzgrp  21572  tgioo3  24765  recvs  25117  recvsOLD  25118  retopn  25351  recms  25352  reust  25353  rrxcph  25364  rrxdsfi  25383  reefgim  26432  amgmlem  26967  nn0omnd  33156  nn0archi  33158  xrge0slmod  33159  ccfldextrr  33471  ccfldsrarelvec  33490  ccfldextdgrr  33491  rezh  33703  rrhcn  33729  rerrext  33741  cnrrext  33742  qqtopn  33743  bj-rveccmod  36912  amgmwlem  48421
  Copyright terms: Public domain W3C validator