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

Definition df-ioo 9890
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 9886 . 2  class  (,)
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 7989 . . 3  class  RR*
52cv 1352 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1352 . . . . . 6  class  z
8 clt 7990 . . . . . 6  class  <
95, 7, 8wbr 4003 . . . . 5  wff  x  < 
z
103cv 1352 . . . . . 6  class  y
117, 10, 8wbr 4003 . . . . 5  wff  z  < 
y
129, 11wa 104 . . . 4  wff  ( x  <  z  /\  z  <  y )
1312, 6, 4crab 2459 . . 3  class  { z  e.  RR*  |  (
x  <  z  /\  z  <  y ) }
142, 3, 4, 4, 13cmpo 5876 . 2  class  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  < 
y ) } )
151, 14wceq 1353 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  9905  iooval  9906  elioo3g  9908  elioo1  9909  iooss1  9914  iooss2  9915  eliooxr  9925  iccssioo  9940  ioossicc  9957  ioossico  9960  iocssioo  9961  icossioo  9962  ioossioo  9963  ioof  9969  ioodisj  9991
  Copyright terms: Public domain W3C validator