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 19769 | . 2 class ℝfld | |
2 | ccnfld 19567 | . . 3 class ℂfld | |
3 | cr 9814 | . . 3 class ℝ | |
4 | cress 15696 | . . 3 class ↾s | |
5 | 2, 3, 4 | co 6549 | . 2 class (ℂfld ↾s ℝ) |
6 | 1, 5 | wceq 1475 | 1 wff ℝfld = (ℂfld ↾s ℝ) |
Colors of variables: wff setvar class |
This definition is referenced by: rebase 19771 remulg 19772 resubdrg 19773 resubgval 19774 replusg 19775 remulr 19776 re0g 19777 re1r 19778 rele2 19779 relt 19780 reds 19781 redvr 19782 retos 19783 refld 19784 refldcj 19785 regsumsupp 19787 tgioo3 22416 recvs 22754 retopn 22975 recms 22976 reust 22977 rrxcph 22988 reefgim 24008 rzgrp 24104 amgmlem 24516 nn0omnd 29172 nn0archi 29174 xrge0slmod 29175 rezh 29343 rrhcn 29369 rerrext 29381 cnrrext 29382 qqtopn 29383 rrxdsfi 39181 amgmwlem 42357 |
Copyright terms: Public domain | W3C validator |