ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-ioo GIF version

Definition df-ioo 9516
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
StepHypRef Expression
1 cioo 9512 . 2 class (,)
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 7671 . . 3 class *
52cv 1298 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1298 . . . . . 6 class 𝑧
8 clt 7672 . . . . . 6 class <
95, 7, 8wbr 3875 . . . . 5 wff 𝑥 < 𝑧
103cv 1298 . . . . . 6 class 𝑦
117, 10, 8wbr 3875 . . . . 5 wff 𝑧 < 𝑦
129, 11wa 103 . . . 4 wff (𝑥 < 𝑧𝑧 < 𝑦)
1312, 6, 4crab 2379 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)}
142, 3, 4, 4, 13cmpo 5708 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
151, 14wceq 1299 1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
Colors of variables: wff set class
This definition is referenced by:  iooex  9531  iooval  9532  elioo3g  9534  elioo1  9535  iooss1  9540  iooss2  9541  eliooxr  9551  iccssioo  9566  ioossicc  9583  ioossico  9586  iocssioo  9587  icossioo  9588  ioossioo  9589  ioof  9595  ioodisj  9617
  Copyright terms: Public domain W3C validator