ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-ioo Unicode version

Definition df-ioo 9279
Description: Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
Assertion
Ref Expression
df-ioo  |-  (,)  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x  <  z  /\  z  <  y ) } )
Distinct variable group:    x, y, z

Detailed syntax breakdown of Definition df-ioo
StepHypRef Expression
1 cioo 9275 . 2  class  (,)
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 7500 . . 3  class  RR*
52cv 1288 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1288 . . . . . 6  class  z
8 clt 7501 . . . . . 6  class  <
95, 7, 8wbr 3837 . . . . 5  wff  x  < 
z
103cv 1288 . . . . . 6  class  y
117, 10, 8wbr 3837 . . . . 5  wff  z  < 
y
129, 11wa 102 . . . 4  wff  ( x  <  z  /\  z  <  y )
1312, 6, 4crab 2363 . . 3  class  { z  e.  RR*  |  (
x  <  z  /\  z  <  y ) }
142, 3, 4, 4, 13cmpt2 5636 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  < 
y ) } )
151, 14wceq 1289 1  wff  (,)  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x  <  z  /\  z  <  y ) } )
Colors of variables: wff set class
This definition is referenced by:  iooex  9294  iooval  9295  elioo3g  9297  elioo1  9298  iooss1  9303  iooss2  9304  eliooxr  9314  iccssioo  9329  ioossicc  9346  ioossico  9349  iocssioo  9350  icossioo  9351  ioossioo  9352  ioof  9358  ioodisj  9379
  Copyright terms: Public domain W3C validator