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

Metamath Proof Explorer

Theorem ioorp

Description: The set of positive reals expressed as an open interval. (Contributed by Steve Rodriguez, 25-Nov-2007)

		Ref	Expression
	Assertion	ioorp	$⊢ (0, +∞) = ℝ^{+}$

Step	Hyp	Ref	Expression
1		ioopos	$⊢ (0, +∞) = \{x \in ℝ \| 0 < x\}$
2		df-rp	$⊢ ℝ^{+} = \{x \in ℝ \| 0 < x\}$
3	1 2	eqtr4i	$⊢ (0, +∞) = ℝ^{+}$