Definition df-icc 11642

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 11638	. 2 class [,]
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cxr 9674	. . 3 class RR*
5	2	cv 1443	. . . . . 6 class x
6		vz	. . . . . . 7 setvar z
7	6	cv 1443	. . . . . 6 class z
8		cle 9676	. . . . . 6 class <_
9	5, 7, 8	wbr 4402	. . . . 5 wff x <_ z
10	3	cv 1443	. . . . . 6 class y
11	7, 10, 8	wbr 4402	. . . . 5 wff z <_ y
12	9, 11	wa 371	. . . 4 wff ( x <_ z /\ z <_ y )
13	12, 6, 4	crab 2741	. . 3 class { z e. RR* | ( x <_ z /\ z <_ y ) }
14	2, 3, 4, 4, 13	cmpt2 6292	. 2 class ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
15	1, 14	wceq 1444	1 wff [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )

This definition is referenced by:  iccval  11675  elicc1  11680  iccss  11702  iccssioo  11703  iccss2  11705  iccssico  11706  iccssxr  11717  ioossicc  11720  icossicc  11721  iocssicc  11722  iccf  11733  snunioo  11758  snunico  11759  snunioc  11760  ioodisj  11762  leordtval2  20228  iccordt  20230  lecldbas  20235  ioombl  22518  itgspliticc  22794  psercnlem2  23379  tanord1  23486  cvmliftlem10  30017  ftc1anclem7  32023  ftc1anclem8  32024  ftc1anc  32025  ioounsn  36094  snunioo2  37606  snunioo1  37613