![]() |
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 20293 | . 2 class ℝfld | |
2 | ccnfld 20091 | . . 3 class ℂfld | |
3 | cr 10525 | . . 3 class ℝ | |
4 | cress 16476 | . . 3 class ↾s | |
5 | 2, 3, 4 | co 7135 | . 2 class (ℂfld ↾s ℝ) |
6 | 1, 5 | wceq 1538 | 1 wff ℝfld = (ℂfld ↾s ℝ) |
Colors of variables: wff setvar class |
This definition is referenced by: rebase 20295 remulg 20296 resubdrg 20297 resubgval 20298 replusg 20299 remulr 20300 re0g 20301 re1r 20302 rele2 20303 relt 20304 reds 20305 redvr 20306 retos 20307 refld 20308 refldcj 20309 regsumsupp 20311 rzgrp 20312 tgioo3 23410 recvs 23751 retopn 23983 recms 23984 reust 23985 rrxcph 23996 rrxdsfi 24015 reefgim 25045 amgmlem 25575 nn0omnd 30965 nn0archi 30967 xrge0slmod 30968 ccfldextrr 31126 ccfldsrarelvec 31144 ccfldextdgrr 31145 rezh 31322 rrhcn 31348 rerrext 31360 cnrrext 31361 qqtopn 31362 bj-rveccmod 34716 amgmwlem 45330 |
Copyright terms: Public domain | W3C validator |