![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-refld | Structured version Visualization version GIF version |
Description: The field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
Ref | Expression |
---|---|
df-refld | ⊢ ℝfld = (ℂfld ↾s ℝ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | crefld 20311 | . 2 class ℝfld | |
2 | ccnfld 20106 | . . 3 class ℂfld | |
3 | cr 10251 | . . 3 class ℝ | |
4 | cress 16223 | . . 3 class ↾s | |
5 | 2, 3, 4 | co 6905 | . 2 class (ℂfld ↾s ℝ) |
6 | 1, 5 | wceq 1656 | 1 wff ℝfld = (ℂfld ↾s ℝ) |
Colors of variables: wff setvar class |
This definition is referenced by: rebase 20313 remulg 20314 resubdrg 20315 resubgval 20316 replusg 20317 remulr 20318 re0g 20319 re1r 20320 rele2 20321 relt 20322 reds 20323 redvr 20324 retos 20325 refld 20326 refldcj 20327 regsumsupp 20329 rzgrp 20330 tgioo3 22978 recvs 23315 retopn 23547 recms 23548 reust 23549 rrxcph 23560 rrxdsfi 23579 reefgim 24603 amgmlem 25129 nn0omnd 30375 nn0archi 30377 xrge0slmod 30378 rezh 30549 rrhcn 30575 rerrext 30587 cnrrext 30588 qqtopn 30589 amgmwlem 43437 |
Copyright terms: Public domain | W3C validator |