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

Definition df-ioc 11563
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 11559 . 2
2 vx . . 3
3 vy . . 3
4 cxr 9648 . . 3
52cv 1394 . . . . . 6
6 vz . . . . . . 7
76cv 1394 . . . . . 6
8 clt 9649 . . . . . 6
95, 7, 8wbr 4452 . . . . 5
103cv 1394 . . . . . 6
11 cle 9650 . . . . . 6
127, 10, 11wbr 4452 . . . . 5
139, 12wa 369 . . . 4
1413, 6, 4crab 2811 . . 3
152, 3, 4, 4, 14cmpt2 6298 . 2
161, 15wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  iocval  11595  elioc1  11600  iocssxr  11637  iocssicc  11641  iocssioo  11643  snunioc  11677  leordtval2  19713  iocpnfordt  19716  lecldbas  19720  pnfnei  19721  iocmnfcld  21276  xrtgioo  21311  ismbf3d  22061  dvloglem  23029  asindmre  30102  dvasin  30103  ioounsn  31177  ioossioc  31524  snunioo2  31544  eliocre  31547  lbioc  31553
  Copyright terms: Public domain W3C validator