Definition df-ioo 13343

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 13339	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11205	. . 3 class ℝ*
5	2	cv 1553	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1553	. . . . . 6 class 𝑧
8		clt 11206	. . . . . 6 class <
9	5, 7, 8	wbr 5094	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1553	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5094	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 398	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3408	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7387	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1554	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  iooex  13362  iooval  13363  ndmioo  13366  elioo3g  13368  iooin  13373  iooss1  13374  iooss2  13375  elioo1  13379  iccssioo  13409  ioossicc  13427  ioossico  13432  iocssioo  13433  icossioo  13434  ioossioo  13435  ioof  13441  ioounsn  13471  snunioo  13472  ioodisj  13476  ioojoin  13477  ioopnfsup  13864  leordtval  23246  icopnfcld  24800  iocmnfcld  24801  bndth  24993  ioombl  25600  ioorf  25608  ioorinv2  25610  ismbf3d  25689  dvfsumrlimge0  26065  dvfsumrlim2  26067  tanord1  26572  dvloglem  26683  rlimcnp  27000  rlimcnp2  27001  dchrisum0lem2a  27551  pnt  27648  joiniooico  32919  tpr2rico  34163  asindmre  38150  dvasin  38151  iocioodisjd  42877  ioossioc  46016  snunioo1  46036  ioossioobi  46041