Metamath Proof Explorer


Definition df-ioo

Description: Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006)

Ref Expression
Assertion df-ioo . = x * , y * z * | x < z z < y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cioo class .
1 vx setvar x
2 cxr class *
3 vy setvar y
4 vz setvar z
5 1 cv setvar x
6 clt class <
7 4 cv setvar z
8 5 7 6 wbr wff x < z
9 3 cv setvar y
10 7 9 6 wbr wff z < y
11 8 10 wa wff x < z z < y
12 11 4 2 crab class z * | x < z z < y
13 1 3 2 2 12 cmpo class x * , y * z * | x < z z < y
14 0 13 wceq wff . = x * , y * z * | x < z z < y