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 [,) +∞ ) ⊆ ℝ

Proof

Step	Hyp	Ref	Expression
1		elrege0	⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
2	1	simplbi	⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) → 𝑥 ∈ ℝ )
3	2	ssriv	⊢ ( 0 [,) +∞ ) ⊆ ℝ