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