![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > df-icc | Unicode version |
Description: Define the set of closed intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
Ref | Expression |
---|---|
df-icc |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cicc 11561 | . 2 | |
2 | vx | . . 3 | |
3 | vy | . . 3 | |
4 | cxr 9648 | . . 3 | |
5 | 2 | cv 1394 | . . . . . 6 |
6 | vz | . . . . . . 7 | |
7 | 6 | cv 1394 | . . . . . 6 |
8 | cle 9650 | . . . . . 6 | |
9 | 5, 7, 8 | wbr 4452 | . . . . 5 |
10 | 3 | cv 1394 | . . . . . 6 |
11 | 7, 10, 8 | wbr 4452 | . . . . 5 |
12 | 9, 11 | wa 369 | . . . 4 |
13 | 12, 6, 4 | crab 2811 | . . 3 |
14 | 2, 3, 4, 4, 13 | cmpt2 6298 | . 2 |
15 | 1, 14 | wceq 1395 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: iccval 11597 elicc1 11602 iccss 11621 iccssioo 11622 iccss2 11624 iccssico 11625 iccssxr 11636 ioossicc 11639 icossicc 11640 iocssicc 11641 iccf 11652 snunioo 11675 snunico 11676 snunioc 11677 ioodisj 11679 leordtval2 19713 iccordt 19715 lecldbas 19720 ioombl 21975 itgspliticc 22243 psercnlem2 22819 tanord1 22924 cvmliftlem10 28739 ftc1anclem7 30096 ftc1anclem8 30097 ftc1anc 30098 ioounsn 31177 snunioo2 31544 snunioo1 31552 |
Copyright terms: Public domain | W3C validator |