Metamath Proof Explorer

Theorem rebase

Description: The base of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017)

Ref Expression
Assertion rebase 
|- RR = ( Base ` RRfld )

Proof

Step Hyp Ref Expression
1 ax-resscn 
 |-  RR C_ CC
2 df-refld 
 |-  RRfld = ( CCfld |`s RR )
3 cnfldbas 
 |-  CC = ( Base ` CCfld )
4 2 3 ressbas2 
 |-  ( RR C_ CC -> RR = ( Base ` RRfld ) )
5 1 4 ax-mp 
 |-  RR = ( Base ` RRfld )