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 } ⊆ ℝ

Proof

Step Hyp Ref Expression
1 0re 0 ∈ ℝ
2 1re 1 ∈ ℝ
3 prssi ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ) → { 0 , 1 } ⊆ ℝ )
4 1 2 3 mp2an { 0 , 1 } ⊆ ℝ