Definition df-ioo 13316

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

Assertion

Ref	Expression
df-ioo	⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-ioo

Step	Hyp	Ref	Expression
1		cioo 13312	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11213	. . 3 class ℝ*
5	2	cv 1539	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1539	. . . . . 6 class 𝑧
8		clt 11214	. . . . . 6 class <
9	5, 7, 8	wbr 5109	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1539	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5109	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 395	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3408	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7391	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1540	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  iooex  13335  iooval  13336  ndmioo  13339  elioo3g  13341  iooin  13346  iooss1  13347  iooss2  13348  elioo1  13352  iccssioo  13382  ioossicc  13400  ioossico  13405  iocssioo  13406  icossioo  13407  ioossioo  13408  ioof  13414  ioounsn  13444  snunioo  13445  ioodisj  13449  ioojoin  13450  ioopnfsup  13832  leordtval  23106  icopnfcld  24661  iocmnfcld  24662  bndth  24863  ioombl  25472  ioorf  25480  ioorinv2  25482  ismbf3d  25561  dvfsumrlimge0  25943  dvfsumrlim2  25945  tanord1  26452  dvloglem  26563  rlimcnp  26881  rlimcnp2  26882  dchrisum0lem2a  27434  pnt  27531  joiniooico  32703  tpr2rico  33908  asindmre  37692  dvasin  37693  iocioodisjd  42303  ioossioc  45483  snunioo1  45503  ioossioobi  45508