Definition df-icc 11535

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 11531	. 2 class [,]
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cxr 9626	. . 3 class RR*
5	2	cv 1378	. . . . . 6 class x
6		vz	. . . . . . 7 setvar z
7	6	cv 1378	. . . . . 6 class z
8		cle 9628	. . . . . 6 class <_
9	5, 7, 8	wbr 4447	. . . . 5 wff x <_ z
10	3	cv 1378	. . . . . 6 class y
11	7, 10, 8	wbr 4447	. . . . 5 wff z <_ y
12	9, 11	wa 369	. . . 4 wff ( x <_ z /\ z <_ y )
13	12, 6, 4	crab 2818	. . 3 class { z e. RR* | ( x <_ z /\ z <_ y ) }
14	2, 3, 4, 4, 13	cmpt2 6285	. 2 class ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
15	1, 14	wceq 1379	1 wff [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )

This definition is referenced by:  iccval  11567  elicc1  11572  iccss  11591  iccssioo  11592  iccss2  11594  iccssico  11595  iccssxr  11606  ioossicc  11609  icossicc  11610  iocssicc  11611  iccf  11622  snunioo  11645  snunico  11646  snunioc  11647  ioodisj  11649  leordtval2  19495  iccordt  19497  lecldbas  19502  ioombl  21726  itg2mulclem  21904  itg2mulc  21905  itgspliticc  21994  psercnlem2  22569  tanord1  22673  cvmliftlem10  28395  ftc1anclem7  29689  ftc1anclem8  29690  ftc1anc  29691  ioounsn  30798  snunioo2  31124  snunioo1  31132