This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rebase

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

		Ref	Expression
	Assertion	rebase	$⊢ ℝ = {Base}_{ℝ_{fld}}$

Step	Hyp	Ref	Expression
1		ax-resscn	$⊢ ℝ \subseteq ℂ$
2		df-refld	$⊢ ℝ_{fld} = ℂ_{fld} ↾_{𝑠} ℝ$
3		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
4	2 3	ressbas2	$⊢ ℝ \subseteq ℂ \to ℝ = {Base}_{ℝ_{fld}}$
5	1 4	ax-mp	$⊢ ℝ = {Base}_{ℝ_{fld}}$