Definition df-icc 11295

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 11291	. 2 class [,]
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cxr 9405	. . 3 class RR*
5	2	cv 1361	. . . . . 6 class x
6		vz	. . . . . . 7 setvar z
7	6	cv 1361	. . . . . 6 class z
8		cle 9407	. . . . . 6 class <_
9	5, 7, 8	wbr 4280	. . . . 5 wff x <_ z
10	3	cv 1361	. . . . . 6 class y
11	7, 10, 8	wbr 4280	. . . . 5 wff z <_ y
12	9, 11	wa 369	. . . 4 wff ( x <_ z /\ z <_ y )
13	12, 6, 4	crab 2709	. . 3 class { z e. RR* | ( x <_ z /\ z <_ y ) }
14	2, 3, 4, 4, 13	cmpt2 6082	. 2 class ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
15	1, 14	wceq 1362	1 wff [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )

This definition is referenced by:  iccval  11327  elicc1  11332  iccss  11351  iccssioo  11352  iccss2  11354  iccssico  11355  iccssxr  11366  ioossicc  11369  iccf  11376  snunioo  11398  snunico  11399  snunioc  11400  ioodisj  11402  leordtval2  18658  iccordt  18660  lecldbas  18665  ioombl  20888  itg2mulclem  21066  itg2mulc  21067  itgspliticc  21156  psercnlem2  21774  tanord1  21878  icossicc  25881  iocssicc  25882  cvmliftlem10  27031  ftc1anclem7  28317  ftc1anclem8  28318  ftc1anc  28319  ioounsn  29430