![]() |
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 21553 | . 2 class ℝfld | |
2 | ccnfld 21296 | . . 3 class ℂfld | |
3 | cr 11139 | . . 3 class ℝ | |
4 | cress 17212 | . . 3 class ↾s | |
5 | 2, 3, 4 | co 7419 | . 2 class (ℂfld ↾s ℝ) |
6 | 1, 5 | wceq 1533 | 1 wff ℝfld = (ℂfld ↾s ℝ) |
Colors of variables: wff setvar class |
This definition is referenced by: rebase 21555 remulg 21556 resubdrg 21557 resubgval 21558 replusg 21559 remulr 21560 re0g 21561 re1r 21562 rele2 21563 relt 21564 reds 21565 redvr 21566 retos 21567 refld 21568 refldcj 21569 regsumsupp 21571 rzgrp 21572 tgioo3 24765 recvs 25117 recvsOLD 25118 retopn 25351 recms 25352 reust 25353 rrxcph 25364 rrxdsfi 25383 reefgim 26432 amgmlem 26967 nn0omnd 33156 nn0archi 33158 xrge0slmod 33159 ccfldextrr 33471 ccfldsrarelvec 33490 ccfldextdgrr 33491 rezh 33703 rrhcn 33729 rerrext 33741 cnrrext 33742 qqtopn 33743 bj-rveccmod 36912 amgmwlem 48421 |
Copyright terms: Public domain | W3C validator |