![]() |
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 21011 | . 2 class ℝfld | |
2 | ccnfld 20799 | . . 3 class ℂfld | |
3 | cr 11051 | . . 3 class ℝ | |
4 | cress 17113 | . . 3 class ↾s | |
5 | 2, 3, 4 | co 7358 | . 2 class (ℂfld ↾s ℝ) |
6 | 1, 5 | wceq 1542 | 1 wff ℝfld = (ℂfld ↾s ℝ) |
Colors of variables: wff setvar class |
This definition is referenced by: rebase 21013 remulg 21014 resubdrg 21015 resubgval 21016 replusg 21017 remulr 21018 re0g 21019 re1r 21020 rele2 21021 relt 21022 reds 21023 redvr 21024 retos 21025 refld 21026 refldcj 21027 regsumsupp 21029 rzgrp 21030 tgioo3 24171 recvs 24512 recvsOLD 24513 retopn 24746 recms 24747 reust 24748 rrxcph 24759 rrxdsfi 24778 reefgim 25812 amgmlem 26342 nn0omnd 32140 nn0archi 32142 xrge0slmod 32143 ccfldextrr 32340 ccfldsrarelvec 32358 ccfldextdgrr 32359 rezh 32555 rrhcn 32581 rerrext 32593 cnrrext 32594 qqtopn 32595 bj-rveccmod 35776 amgmwlem 47256 |
Copyright terms: Public domain | W3C validator |