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

Metamath Proof Explorer

Theorem iooex

Description: The set of open intervals of extended reals exists. (Contributed by NM, 6-Feb-2007) (Revised by Mario Carneiro, 3-Nov-2013)

		Ref	Expression
	Assertion	iooex	$⊢ (.) \in V$

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