Definition df-ioo 13266

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 13262	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11166	. . 3 class ℝ*
5	2	cv 1541	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1541	. . . . . 6 class 𝑧
8		clt 11167	. . . . . 6 class <
9	5, 7, 8	wbr 5086	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1541	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5086	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 395	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3390	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7360	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1542	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  iooex  13285  iooval  13286  ndmioo  13289  elioo3g  13291  iooin  13296  iooss1  13297  iooss2  13298  elioo1  13302  iccssioo  13332  ioossicc  13350  ioossico  13355  iocssioo  13356  icossioo  13357  ioossioo  13358  ioof  13364  ioounsn  13394  snunioo  13395  ioodisj  13399  ioojoin  13400  ioopnfsup  13785  leordtval  23156  icopnfcld  24710  iocmnfcld  24711  bndth  24903  ioombl  25510  ioorf  25518  ioorinv2  25520  ismbf3d  25599  dvfsumrlimge0  25978  dvfsumrlim2  25980  tanord1  26486  dvloglem  26597  rlimcnp  26915  rlimcnp2  26916  dchrisum0lem2a  27468  pnt  27565  joiniooico  32837  tpr2rico  34062  asindmre  38015  dvasin  38016  iocioodisjd  42751  ioossioc  45926  snunioo1  45946  ioossioobi  45951