Definition df-icc 12182

Description: Define the set of closed intervals of extended reals. (Contributed by NM, 24-Dec-2006.)

Assertion

Ref	Expression
df-icc	|- [,] = ( 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-icc

Step	Hyp	Ref	Expression
1		cicc 12178	. 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		cle 10075	. . . . . 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:  iccval  12214  elicc1  12219  iccss  12241  iccssioo  12242  iccss2  12244  iccssico  12245  iccssxr  12256  ioossicc  12259  icossicc  12260  iocssicc  12261  iccf  12272  snunioo  12298  snunico  12299  snunioc  12300  ioodisj  12302  leordtval2  21016  iccordt  21018  lecldbas  21023  ioombl  23333  itgspliticc  23603  psercnlem2  24178  tanord1  24283  cvmliftlem10  31276  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  ioounsn  37795  snunioo2  39731  snunioo1  39738