Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-icc Unicode version

Definition df-icc 11565
 Description: Define the set of closed intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
Assertion
Ref Expression
df-icc
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-icc
StepHypRef Expression
1 cicc 11561 . 2
2 vx . . 3
3 vy . . 3
4 cxr 9648 . . 3
52cv 1394 . . . . . 6
6 vz . . . . . . 7
76cv 1394 . . . . . 6
8 cle 9650 . . . . . 6
95, 7, 8wbr 4452 . . . . 5
103cv 1394 . . . . . 6
117, 10, 8wbr 4452 . . . . 5
129, 11wa 369 . . . 4
1312, 6, 4crab 2811 . . 3
142, 3, 4, 4, 13cmpt2 6298 . 2
151, 14wceq 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