Metamath Proof Explorer

Theorem elunitrn

Description: The closed unit interval is a subset of the set of the real numbers. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 21-Dec-2016)

		Ref	Expression
	Assertion	elunitrn	$⊢ A \in [0, 1] \to A \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		elicc01	$⊢ A \in [0, 1] \leftrightarrow (A \in ℝ \land 0 \leq A \land A \leq 1)$
2	1	simp1bi	$⊢ A \in [0, 1] \to A \in ℝ$