Definition df-ioo 13364

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 13360	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11266	. . 3 class ℝ*
5	2	cv 1539	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1539	. . . . . 6 class 𝑧
8		clt 11267	. . . . . 6 class <
9	5, 7, 8	wbr 5119	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1539	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5119	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 395	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3415	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7405	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1540	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  iooex  13383  iooval  13384  ndmioo  13387  elioo3g  13389  iooin  13394  iooss1  13395  iooss2  13396  elioo1  13400  iccssioo  13430  ioossicc  13448  ioossico  13453  iocssioo  13454  icossioo  13455  ioossioo  13456  ioof  13462  ioounsn  13492  snunioo  13493  ioodisj  13497  ioojoin  13498  ioopnfsup  13879  leordtval  23149  icopnfcld  24704  iocmnfcld  24705  bndth  24906  ioombl  25516  ioorf  25524  ioorinv2  25526  ismbf3d  25605  dvfsumrlimge0  25987  dvfsumrlim2  25989  tanord1  26496  dvloglem  26607  rlimcnp  26925  rlimcnp2  26926  dchrisum0lem2a  27478  pnt  27575  joiniooico  32697  tpr2rico  33889  asindmre  37673  dvasin  37674  iocioodisjd  42316  ioossioc  45469  snunioo1  45489  ioossioobi  45494