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	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left[A,B\right]=\left\{x\in {ℝ}^{*}|\left(A\le x\wedge x\le B\right)\right\}$$

Proof

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