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 01

Proof

Step Hyp Ref Expression
1 0re 0
2 1re 1
3 iccssre 0101
4 1 2 3 mp2an 01