Theorem icoval

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

	Ref	Expression
Assertion	icoval	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left[A,B\right)=\left\{x\in {ℝ}^{*}|\left(A\le x\wedge x<B\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-ico	$$⊢\left[.\right)=\left(y\in {ℝ}^{*},z\in {ℝ}^{*}⟼\left\{x\in {ℝ}^{*}|\left(y\le x\wedge x<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<B\right)\right\}$$