Description: ( 0 , 1 ) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | unitssre | |- ( 0 [,] 1 ) C_ RR |
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 |