Definition df-ioo 13375

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 13371	. 2 class (,)
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11241	. . 3 class ℝ*
5	2	cv 1567	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1567	. . . . . 6 class 𝑧
8		clt 11242	. . . . . 6 class <
9	5, 7, 8	wbr 5108	. . . . 5 wff 𝑥 < 𝑧
10	3	cv 1567	. . . . . 6 class 𝑦
11	7, 10, 8	wbr 5108	. . . . 5 wff 𝑧 < 𝑦
12	9, 11	wa 400	. . . 4 wff (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)
13	12, 6, 4	crab 3414	. . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}
14	2, 3, 4, 4, 13	cmpo 7412	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
15	1, 14	wceq 1568	1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})

This definition is referenced by:  iooex  13394  iooval  13395  ndmioo  13398  elioo3g  13400  iooin  13405  iooss1  13406  iooss2  13407  elioo1  13411  iccssioo  13441  ioossicc  13459  ioossico  13464  iocssioo  13465  icossioo  13466  ioossioo  13467  ioof  13473  ioounsn  13503  snunioo  13504  ioodisj  13508  ioojoin  13509  ioopnfsup  13897  leordtval  23349  icopnfcld  24903  iocmnfcld  24904  bndth  25096  ioombl  25703  ioorf  25711  ioorinv2  25713  ismbf3d  25792  dvfsumrlimge0  26168  dvfsumrlim2  26170  tanord1  26678  dvloglem  26789  rlimcnp  27106  rlimcnp2  27107  dchrisum0lem2a  27657  pnt  27754  joiniooico  33085  tpr2rico  34268  asindmre  38320  dvasin  38321  iocioodisjd  43049  ioossioc  46178  snunioo1  46198  ioossioobi  46203