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

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

Detailed syntax breakdown of Definition df-ioc
StepHypRef Expression
1 cioc 10909 . 2
2 vx . . 3
3 vy . . 3
4 cxr 9111 . . 3
52cv 1651 . . . . . 6
6 vz . . . . . . 7
76cv 1651 . . . . . 6
8 clt 9112 . . . . . 6
95, 7, 8wbr 4204 . . . . 5
103cv 1651 . . . . . 6
11 cle 9113 . . . . . 6
127, 10, 11wbr 4204 . . . . 5
139, 12wa 359 . . . 4
1413, 6, 4crab 2701 . . 3
152, 3, 4, 4, 14cmpt2 6075 . 2
161, 15wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  iocval  10945  elioc1  10950  iocssxr  10986  leordtval2  17268  iocpnfordt  17271  lecldbas  17275  pnfnei  17276  iocmnfcld  18795  xrtgioo  18829  ismbf3d  19538  dvloglem  20531  iocssicc  24122  iocssioo  24124  snunioc  24129
 Copyright terms: Public domain W3C validator