Metamath Proof Explorer

Theorem iooex

Description: The set of open intervals of extended reals exists. (Contributed by NM, 6-Feb-2007) (Revised by Mario Carneiro, 3-Nov-2013)

Ref Expression
Assertion iooex 
|- (,) e. _V

Proof

Step Hyp Ref Expression
1 df-ioo 
 |-  (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
2 1 ixxex 
 |-  (,) e. _V