Metamath Proof Explorer

Theorem unitssre

Description: ( 0 , 1 ) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Assertion unitssre 
|- ( 0 [,] 1 ) C_ RR

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 1re 
 |-  1 e. RR
3 iccssre 
 |-  ( ( 0 e. RR /\ 1 e. RR ) -> ( 0 [,] 1 ) C_ RR )
4 1 2 3 mp2an 
 |-  ( 0 [,] 1 ) C_ RR