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

Definition df-ioo 9068
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 9064 . 2  class  (,)
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 7291 . . 3  class  RR*
52cv 1284 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1284 . . . . . 6  class  z
8 clt 7292 . . . . . 6  class  <
95, 7, 8wbr 3806 . . . . 5  wff  x  < 
z
103cv 1284 . . . . . 6  class  y
117, 10, 8wbr 3806 . . . . 5  wff  z  < 
y
129, 11wa 102 . . . 4  wff  ( x  <  z  /\  z  <  y )
1312, 6, 4crab 2357 . . 3  class  { z  e.  RR*  |  (
x  <  z  /\  z  <  y ) }
142, 3, 4, 4, 13cmpt2 5567 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  < 
y ) } )
151, 14wceq 1285 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  9083  iooval  9084  elioo3g  9086  elioo1  9087  iooss1  9092  iooss2  9093  eliooxr  9103  iccssioo  9118  ioossicc  9135  ioossico  9138  iocssioo  9139  icossioo  9140  ioossioo  9141  ioof  9147  ioodisj  9168
  Copyright terms: Public domain W3C validator