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

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

Detailed syntax breakdown of Definition df-ioo
StepHypRef Expression
1 cioo 11558 . 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
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:  iooex  11581  iooval  11582  ndmioo  11585  elioo3g  11587  iooin  11592  iooss1  11593  iooss2  11594  elioo1  11598  iccssioo  11622  ioossicc  11639  ioossico  11642  iocssioo  11643  icossioo  11644  ioossioo  11645  ioof  11651  snunioo  11675  ioodisj  11679  ioojoin  11680  ioopnfsup  11991  leordtval  19714  icopnfcld  21275  iocmnfcld  21276  bndth  21458  ioombl  21975  ioorf  21982  ioorinv2  21984  ismbf3d  22061  dvfsumrlimge0  22431  dvfsumrlim2  22433  tanord1  22924  dvloglem  23029  rlimcnp  23295  rlimcnp2  23296  dchrisum0lem2a  23702  pnt  23799  joiniooico  27585  tpr2rico  27894  asindmre  30102  dvasin  30103  ioounsn  31177  ioossioc  31524  snunioo2  31544  snunioo1  31552  ioossioobi  31557
  Copyright terms: Public domain W3C validator