Metamath Proof Explorer

Definition df-refld

Description: The field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019)

Ref Expression
Assertion df-refld 
|- RRfld = ( CCfld |`s RR )

Detailed syntax breakdown

Step Hyp Ref Expression
0 crefld 
 |-  RRfld
1 ccnfld 
 |-  CCfld
2 cress 
 |-  |`s
3 cr 
 |-  RR
4 1 3 2 co 
 |-  ( CCfld |`s RR )
5 0 4 wceq 
 |-  RRfld = ( CCfld |`s RR )