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 ↾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 ℝ )