Definition df-icc 11565

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

Assertion

Ref	Expression
df-icc

Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-icc

Step	Hyp	Ref	Expression
1		cicc 11561	. 2
2		vx	. . 3
3		vy	. . 3
4		cxr 9648	. . 3
5	2	cv 1394	. . . . . 6
6		vz	. . . . . . 7
7	6	cv 1394	. . . . . 6
8		cle 9650	. . . . . 6
9	5, 7, 8	wbr 4452	. . . . 5
10	3	cv 1394	. . . . . 6
11	7, 10, 8	wbr 4452	. . . . 5
12	9, 11	wa 369	. . . 4
13	12, 6, 4	crab 2811	. . 3
14	2, 3, 4, 4, 13	cmpt2 6298	. 2
15	1, 14	wceq 1395	1

This definition is referenced by:  iccval  11597  elicc1  11602  iccss  11621  iccssioo  11622  iccss2  11624  iccssico  11625  iccssxr  11636  ioossicc  11639  icossicc  11640  iocssicc  11641  iccf  11652  snunioo  11675  snunico  11676  snunioc  11677  ioodisj  11679  leordtval2  19713  iccordt  19715  lecldbas  19720  ioombl  21975  itgspliticc  22243  psercnlem2  22819  tanord1  22924  cvmliftlem10  28739  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  ioounsn  31177  snunioo2  31544  snunioo1  31552