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

Definition df-ioo 9242
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 9238 . 2 class (,)
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 7465 . . 3 class *
52cv 1286 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1286 . . . . . 6 class 𝑧
8 clt 7466 . . . . . 6 class <
95, 7, 8wbr 3820 . . . . 5 wff 𝑥 < 𝑧
103cv 1286 . . . . . 6 class 𝑦
117, 10, 8wbr 3820 . . . . 5 wff 𝑧 < 𝑦
129, 11wa 102 . . . 4 wff (𝑥 < 𝑧𝑧 < 𝑦)
1312, 6, 4crab 2359 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)}
142, 3, 4, 4, 13cmpt2 5615 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
151, 14wceq 1287 1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
Colors of variables: wff set class
This definition is referenced by:  iooex  9257  iooval  9258  elioo3g  9260  elioo1  9261  iooss1  9266  iooss2  9267  eliooxr  9277  iccssioo  9292  ioossicc  9309  ioossico  9312  iocssioo  9313  icossioo  9314  ioossioo  9315  ioof  9321  ioodisj  9342
  Copyright terms: Public domain W3C validator