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

Definition df-icc 10816
 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 10812 . 2
2 vx . . 3
3 vy . . 3
4 cxr 9013 . . 3
52cv 1646 . . . . . 6
6 vz . . . . . . 7
76cv 1646 . . . . . 6
8 cle 9015 . . . . . 6
95, 7, 8wbr 4125 . . . . 5
103cv 1646 . . . . . 6
117, 10, 8wbr 4125 . . . . 5
129, 11wa 358 . . . 4
1312, 6, 4crab 2632 . . 3
142, 3, 4, 4, 13cmpt2 5983 . 2
151, 14wceq 1647 1
 Colors of variables: wff set class This definition is referenced by:  iccval  10848  elicc1  10853  iccss  10871  iccssioo  10872  iccss2  10873  iccssico  10874  iccssxr  10885  ioossicc  10888  iccf  10895  snunioo  10915  snunico  10916  ioodisj  10918  leordtval2  17159  iccordt  17161  lecldbas  17166  ioombl  19137  itg2mulclem  19316  itg2mulc  19317  itgspliticc  19406  psercnlem2  20018  tanord1  20117  icossicc  23529  iocssicc  23530  snunioc  23538  cvmliftlem10  24428  itg2addnc  25677
 Copyright terms: Public domain W3C validator