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

Definition df-ioo 8761
 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 8757 . 2 class (,)
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cxr 7059 . . 3 class *
52cv 1242 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1242 . . . . . 6 class 𝑧
8 clt 7060 . . . . . 6 class <
95, 7, 8wbr 3764 . . . . 5 wff 𝑥 < 𝑧
103cv 1242 . . . . . 6 class 𝑦
117, 10, 8wbr 3764 . . . . 5 wff 𝑧 < 𝑦
129, 11wa 97 . . . 4 wff (𝑥 < 𝑧𝑧 < 𝑦)
1312, 6, 4crab 2310 . . 3 class {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)}
142, 3, 4, 4, 13cmpt2 5514 . 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
151, 14wceq 1243 1 wff (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
 Colors of variables: wff set class This definition is referenced by:  iooex  8776  iooval  8777  elioo3g  8779  elioo1  8780  iooss1  8785  iooss2  8786  eliooxr  8796  iccssioo  8811  ioossicc  8828  ioossico  8831  iocssioo  8832  icossioo  8833  ioossioo  8834  ioof  8840  ioodisj  8861
 Copyright terms: Public domain W3C validator