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

Metamath Proof Explorer

Theorem iccval

Description: Value of the closed interval function. (Contributed by NM, 24-Dec-2006) (Revised by Mario Carneiro, 3-Nov-2013)

		Ref	Expression
	Assertion	iccval	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to [A, B] = \{x \in ℝ^{*} \| (A \leq x \land x \leq B)\}$

Step	Hyp	Ref	Expression
1		df-icc	$⊢ [.] = (y \in ℝ^{}, z \in ℝ^{} ⟼ \{x \in ℝ^{*} \| (y \leq x \land x \leq z)\})$
2	1	ixxval	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to [A, B] = \{x \in ℝ^{*} \| (A \leq x \land x \leq B)\}$