Metamath Proof Explorer

Theorem elicc01

Description: Membership in the closed real interval between 0 and 1, also called the closed unit interval. (Contributed by AV, 20-Aug-2022)

Ref Expression
Assertion elicc01 
|- ( X e. ( 0 [,] 1 ) <-> ( X e. RR /\ 0 <_ X /\ X <_ 1 ) )

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 1re 
 |-  1 e. RR
3 1 2 elicc2i 
 |-  ( X e. ( 0 [,] 1 ) <-> ( X e. RR /\ 0 <_ X /\ X <_ 1 ) )