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

Metamath Proof Explorer

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	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A, B) = \{x \in ℝ^{*} \| (A < x \land x < B)\}$

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