Metamath Proof Explorer

Theorem pr01ssre

Description: The range of the indicator function is a subset of RR . (Contributed by Thierry Arnoux, 14-Aug-2017)

Ref Expression
Assertion pr01ssre 
|- { 0 , 1 } C_ RR

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 1re 
 |-  1 e. RR
3 prssi 
 |-  ( ( 0 e. RR /\ 1 e. RR ) -> { 0 , 1 } C_ RR )
4 1 2 3 mp2an 
 |-  { 0 , 1 } C_ RR