This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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, +∞) \subseteq ℝ$

Step	Hyp	Ref	Expression
1		elrege0	$⊢ x \in [0, +∞) \leftrightarrow (x \in ℝ \land 0 \leq x)$
2	1	simplbi	$⊢ x \in [0, +∞) \to x \in ℝ$
3	2	ssriv	$⊢ [0, +∞) \subseteq ℝ$