Definition df-ioo 12179

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

Step	Hyp	Ref	Expression
1		cioo 12175	. 2 class (,)
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cxr 10073	. . 3 class RR*
5	2	cv 1482	. . . . . 6 class x
6		vz	. . . . . . 7 setvar z
7	6	cv 1482	. . . . . 6 class z
8		clt 10074	. . . . . 6 class <
9	5, 7, 8	wbr 4653	. . . . 5 wff x < z
10	3	cv 1482	. . . . . 6 class y
11	7, 10, 8	wbr 4653	. . . . 5 wff z < y
12	9, 11	wa 384	. . . 4 wff ( x < z /\ z < y )
13	12, 6, 4	crab 2916	. . 3 class { z e. RR* | ( x < z /\ z < y ) }
14	2, 3, 4, 4, 13	cmpt2 6652	. 2 class ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
15	1, 14	wceq 1483	1 wff (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )

This definition is referenced by:  iooex  12198  iooval  12199  ndmioo  12202  elioo3g  12204  iooin  12209  iooss1  12210  iooss2  12211  elioo1  12215  iccssioo  12242  ioossicc  12259  ioossico  12262  iocssioo  12263  icossioo  12264  ioossioo  12265  ioof  12271  snunioo  12298  ioodisj  12302  ioojoin  12303  ioopnfsup  12663  leordtval  21017  icopnfcld  22571  iocmnfcld  22572  bndth  22757  ioombl  23333  ioorf  23341  ioorinv2  23343  ismbf3d  23421  dvfsumrlimge0  23793  dvfsumrlim2  23795  tanord1  24283  dvloglem  24394  rlimcnp  24692  rlimcnp2  24693  dchrisum0lem2a  25206  pnt  25303  joiniooico  29536  tpr2rico  29958  asindmre  33495  dvasin  33496  ioounsn  37795  ioossioc  39713  snunioo2  39731  snunioo1  39738  ioossioobi  39743