Metamath Proof Explorer

Theorem iocval

Description: Value of the open-below, closed-above interval function. (Contributed by NM, 24-Dec-2006) (Revised by Mario Carneiro, 3-Nov-2013)

Ref Expression
Assertion iocval 
|- ( ( A e. RR* /\ B e. RR* ) -> ( A (,] B ) = { x e. RR* | ( A < x /\ x <_ B ) } )

Proof

Step Hyp Ref Expression
1 df-ioc 
 |-  (,] = ( y e. RR* , z e. RR* |-> { x e. RR* | ( y < x /\ x <_ z ) } )
2 1 ixxval 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A (,] B ) = { x e. RR* | ( A < x /\ x <_ B ) } )