Definition df-ioo 13255

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 13251	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11151	. . 3 class ℝ*
5	2	cv 1540	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1540	. . . . . 6 class 𝑧
8		clt 11152	. . . . . 6 class <
9	5, 7, 8	wbr 5093	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1540	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5093	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 395	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3395	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7354	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1541	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  iooex  13274  iooval  13275  ndmioo  13278  elioo3g  13280  iooin  13285  iooss1  13286  iooss2  13287  elioo1  13291  iccssioo  13321  ioossicc  13339  ioossico  13344  iocssioo  13345  icossioo  13346  ioossioo  13347  ioof  13353  ioounsn  13383  snunioo  13384  ioodisj  13388  ioojoin  13389  ioopnfsup  13774  leordtval  23134  icopnfcld  24688  iocmnfcld  24689  bndth  24890  ioombl  25499  ioorf  25507  ioorinv2  25509  ismbf3d  25588  dvfsumrlimge0  25970  dvfsumrlim2  25972  tanord1  26479  dvloglem  26590  rlimcnp  26908  rlimcnp2  26909  dchrisum0lem2a  27461  pnt  27558  joiniooico  32764  tpr2rico  33932  asindmre  37749  dvasin  37750  iocioodisjd  42419  ioossioc  45597  snunioo1  45617  ioossioobi  45622