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

Definition df-ioo 9698
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 9694 . 2 class (,)
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 7818 . . 3 class *
52cv 1330 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1330 . . . . . 6 class 𝑧
8 clt 7819 . . . . . 6 class <
95, 7, 8wbr 3932 . . . . 5 wff 𝑥 < 𝑧
103cv 1330 . . . . . 6 class 𝑦
117, 10, 8wbr 3932 . . . . 5 wff 𝑧 < 𝑦
129, 11wa 103 . . . 4 wff (𝑥 < 𝑧𝑧 < 𝑦)
1312, 6, 4crab 2420 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)}
142, 3, 4, 4, 13cmpo 5779 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
151, 14wceq 1331 1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
Colors of variables: wff set class
This definition is referenced by:  iooex  9713  iooval  9714  elioo3g  9716  elioo1  9717  iooss1  9722  iooss2  9723  eliooxr  9733  iccssioo  9748  ioossicc  9765  ioossico  9768  iocssioo  9769  icossioo  9770  ioossioo  9771  ioof  9777  ioodisj  9799
  Copyright terms: Public domain W3C validator