Theorem rebase

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

	Ref	Expression
Assertion	rebase	⊢ ℝ = ( Base ‘ ℝfld )

Proof

Step	Hyp	Ref	Expression
1		ax-resscn	⊢ ℝ ⊆ ℂ
2		df-refld	⊢ ℝfld = ( ℂfld ↾s ℝ )
3		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
4	2 3	ressbas2	⊢ ( ℝ ⊆ ℂ → ℝ = ( Base ‘ ℝfld ) )
5	1 4	ax-mp	⊢ ℝ = ( Base ‘ ℝfld )