Theorem iooval

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

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

Proof

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