Metamath Proof Explorer

Theorem rge0ssre

Description: Nonnegative real numbers are real numbers. (Contributed by Thierry Arnoux, 9-Sep-2018) (Proof shortened by AV, 8-Sep-2019)

Ref Expression
Assertion rge0ssre 
|- ( 0 [,) +oo ) C_ RR

Proof

Step Hyp Ref Expression
1 elrege0 
 |-  ( x e. ( 0 [,) +oo ) <-> ( x e. RR /\ 0 <_ x ) )
2 1 simplbi 
 |-  ( x e. ( 0 [,) +oo ) -> x e. RR )
3 2 ssriv 
 |-  ( 0 [,) +oo ) C_ RR