| 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 21622 | . 2 class ℝfld | |
| 2 | ccnfld 21364 | . . 3 class ℂfld | |
| 3 | cr 11154 | . . 3 class ℝ | |
| 4 | cress 17274 | . . 3 class ↾s | |
| 5 | 2, 3, 4 | co 7431 | . 2 class (ℂfld ↾s ℝ) |
| 6 | 1, 5 | wceq 1540 | 1 wff ℝfld = (ℂfld ↾s ℝ) |
| Colors of variables: wff setvar class |
| This definition is referenced by: rebase 21624 remulg 21625 resubdrg 21626 resubgval 21627 replusg 21628 remulr 21629 re0g 21630 re1r 21631 rele2 21632 relt 21633 reds 21634 redvr 21635 retos 21636 refld 21637 refldcj 21638 regsumsupp 21640 rzgrp 21641 tgioo3 24827 recvs 25179 recvsOLD 25180 retopn 25413 recms 25414 reust 25415 rrxcph 25426 rrxdsfi 25445 reefgim 26494 amgmlem 27033 nn0omnd 33373 nn0archi 33375 xrge0slmod 33376 ccfldextrr 33699 ccfldsrarelvec 33721 ccfldextdgrr 33722 rezh 33970 rrhcn 33998 rerrext 34010 cnrrext 34011 qqtopn 34012 bj-rveccmod 37303 amgmwlem 49321 |
| Copyright terms: Public domain | W3C validator |