Definition df-refld

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

	Ref	Expression
Assertion	df-refld	⊢ ℝfld = ( ℂfld ↾s ℝ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crefld	⊢ ℝfld
1		ccnfld	⊢ ℂfld
2		cress	⊢ ↾s
3		cr	⊢ ℝ
4	1 3 2	co	⊢ ( ℂfld ↾s ℝ )
5	0 4	wceq	⊢ ℝfld = ( ℂfld ↾s ℝ )