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

Metamath Proof Explorer

Theorem elicc01

Description: Membership in the closed real interval between 0 and 1, also called the closed unit interval. (Contributed by AV, 20-Aug-2022)

		Ref	Expression
	Assertion	elicc01	$⊢ X \in [0, 1] \leftrightarrow (X \in ℝ \land 0 \leq X \land X \leq 1)$

Step	Hyp	Ref	Expression
1		0re	$⊢ 0 \in ℝ$
2		1re	$⊢ 1 \in ℝ$
3	1 2	elicc2i	$⊢ X \in [0, 1] \leftrightarrow (X \in ℝ \land 0 \leq X \land X \leq 1)$