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

Definition df-ioo 9922
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 9918 . 2 class (,)
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 8021 . . 3 class *
52cv 1363 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1363 . . . . . 6 class 𝑧
8 clt 8022 . . . . . 6 class <
95, 7, 8wbr 4018 . . . . 5 wff 𝑥 < 𝑧
103cv 1363 . . . . . 6 class 𝑦
117, 10, 8wbr 4018 . . . . 5 wff 𝑧 < 𝑦
129, 11wa 104 . . . 4 wff (𝑥 < 𝑧𝑧 < 𝑦)
1312, 6, 4crab 2472 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)}
142, 3, 4, 4, 13cmpo 5898 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
151, 14wceq 1364 1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
Colors of variables: wff set class
This definition is referenced by:  iooex  9937  iooval  9938  elioo3g  9940  elioo1  9941  iooss1  9946  iooss2  9947  eliooxr  9957  iccssioo  9972  ioossicc  9989  ioossico  9992  iocssioo  9993  icossioo  9994  ioossioo  9995  ioof  10001  ioodisj  10023
  Copyright terms: Public domain W3C validator