Definition df-ioo 13300

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 13296	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11176	. . 3 class ℝ*
5	2	cv 1546	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1546	. . . . . 6 class 𝑧
8		clt 11177	. . . . . 6 class <
9	5, 7, 8	wbr 5079	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1546	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5079	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 396	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3392	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7365	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1547	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  iooex  13319  iooval  13320  ndmioo  13323  elioo3g  13325  iooin  13330  iooss1  13331  iooss2  13332  elioo1  13336  iccssioo  13366  ioossicc  13384  ioossico  13389  iocssioo  13390  icossioo  13391  ioossioo  13392  ioof  13398  ioounsn  13428  snunioo  13429  ioodisj  13433  ioojoin  13434  ioopnfsup  13821  leordtval  23203  icopnfcld  24757  iocmnfcld  24758  bndth  24950  ioombl  25557  ioorf  25565  ioorinv2  25567  ismbf3d  25646  dvfsumrlimge0  26022  dvfsumrlim2  26024  tanord1  26526  dvloglem  26637  rlimcnp  26954  rlimcnp2  26955  dchrisum0lem2a  27505  pnt  27602  joiniooico  32873  tpr2rico  34103  asindmre  38071  dvasin  38072  iocioodisjd  42798  ioossioc  45938  snunioo1  45958  ioossioobi  45963