Theorem iocval

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

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

Proof

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