Definition df-icc 11421

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 11417	. 2 class [,]
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cxr 9531	. . 3 class RR*
5	2	cv 1369	. . . . . 6 class x
6		vz	. . . . . . 7 setvar z
7	6	cv 1369	. . . . . 6 class z
8		cle 9533	. . . . . 6 class <_
9	5, 7, 8	wbr 4403	. . . . 5 wff x <_ z
10	3	cv 1369	. . . . . 6 class y
11	7, 10, 8	wbr 4403	. . . . 5 wff z <_ y
12	9, 11	wa 369	. . . 4 wff ( x <_ z /\ z <_ y )
13	12, 6, 4	crab 2803	. . 3 class { z e. RR* | ( x <_ z /\ z <_ y ) }
14	2, 3, 4, 4, 13	cmpt2 6205	. 2 class ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
15	1, 14	wceq 1370	1 wff [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )

This definition is referenced by:  iccval  11453  elicc1  11458  iccss  11477  iccssioo  11478  iccss2  11480  iccssico  11481  iccssxr  11492  ioossicc  11495  icossicc  11496  iocssicc  11497  iccf  11508  snunioo  11531  snunico  11532  snunioc  11533  ioodisj  11535  leordtval2  18951  iccordt  18953  lecldbas  18958  ioombl  21182  itg2mulclem  21360  itg2mulc  21361  itgspliticc  21450  psercnlem2  22025  tanord1  22129  cvmliftlem10  27347  ftc1anclem7  28641  ftc1anclem8  28642  ftc1anc  28643  ioounsn  29753