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

Definition df-ioo 8531
Description: Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
Assertion
Ref Expression
df-ioo (,) = (x *, y * ↦ {z * ∣ (x < z z < y)})
Distinct variable group:   x,y,z

Detailed syntax breakdown of Definition df-ioo
StepHypRef Expression
1 cioo 8527 . 2 class (,)
2 vx . . 3 setvar x
3 vy . . 3 setvar y
4 cxr 6856 . . 3 class *
52cv 1241 . . . . . 6 class x
6 vz . . . . . . 7 setvar z
76cv 1241 . . . . . 6 class z
8 clt 6857 . . . . . 6 class <
95, 7, 8wbr 3755 . . . . 5 wff x < z
103cv 1241 . . . . . 6 class y
117, 10, 8wbr 3755 . . . . 5 wff z < y
129, 11wa 97 . . . 4 wff (x < z z < y)
1312, 6, 4crab 2304 . . 3 class {z * ∣ (x < z z < y)}
142, 3, 4, 4, 13cmpt2 5457 . 2 class (x *, y * ↦ {z * ∣ (x < z z < y)})
151, 14wceq 1242 1 wff (,) = (x *, y * ↦ {z * ∣ (x < z z < y)})
Colors of variables: wff set class
This definition is referenced by:  iooex  8546  iooval  8547  elioo3g  8549  elioo1  8550  iooss1  8555  iooss2  8556  eliooxr  8566  iccssioo  8581  ioossicc  8598  ioossico  8601  iocssioo  8602  icossioo  8603  ioossioo  8604  ioof  8610  ioodisj  8631
  Copyright terms: Public domain W3C validator