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

Metamath Proof Explorer

Definition df-refld

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

		Ref	Expression
	Assertion	df-refld	$⊢ ℝ_{fld} = ℂ_{fld} ↾_{𝑠} ℝ$

Step	Hyp	Ref	Expression
0		crefld	$class ℝ_{fld}$
1		ccnfld	$class ℂ_{fld}$
2		cress	$class ↾_{𝑠}$
3		cr	$class ℝ$
4	1 3 2	co	$class (ℂ_{fld} ↾_{𝑠} ℝ)$
5	0 4	wceq	$wff ℝ_{fld} = ℂ_{fld} ↾_{𝑠} ℝ$