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

Metamath Proof Explorer

Theorem elrp

Description: Membership in the set of positive reals. (Contributed by NM, 27-Oct-2007)

		Ref	Expression
	Assertion	elrp	$⊢ A \in ℝ^{+} \leftrightarrow (A \in ℝ \land 0 < A)$

Step	Hyp	Ref	Expression
1		breq2	$⊢ x = A \to (0 < x \leftrightarrow 0 < A)$
2		df-rp	$⊢ ℝ^{+} = \{x \in ℝ \| 0 < x\}$
3	1 2	elrab2	$⊢ A \in ℝ^{+} \leftrightarrow (A \in ℝ \land 0 < A)$