Metamath Proof Explorer


Theorem iooval2

Description: Value of the open interval function. (Contributed by NM, 6-Feb-2007) (Revised by Mario Carneiro, 3-Nov-2013)

Ref Expression
Assertion iooval2 A * B * A B = x | A < x x < B

Proof

Step Hyp Ref Expression
1 iooval A * B * A B = x * | A < x x < B
2 elioore x A B x
3 2 ssriv A B
4 1 3 eqsstrrdi A * B * x * | A < x x < B
5 df-ss x * | A < x x < B x * | A < x x < B = x * | A < x x < B
6 4 5 sylib A * B * x * | A < x x < B = x * | A < x x < B
7 inrab2 x * | A < x x < B = x * | A < x x < B
8 ressxr *
9 sseqin2 * * =
10 8 9 mpbi * =
11 10 rabeqi x * | A < x x < B = x | A < x x < B
12 7 11 eqtri x * | A < x x < B = x | A < x x < B
13 6 12 eqtr3di A * B * x * | A < x x < B = x | A < x x < B
14 1 13 eqtrd A * B * A B = x | A < x x < B