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

Metamath Proof Explorer

Theorem elrpd

Description: Membership in the set of positive reals. (Contributed by Mario Carneiro, 28-May-2016)

Step	Hyp	Ref	Expression
1		elrpd.1	$⊢ φ \to A \in ℝ$
2		elrpd.2	$⊢ φ \to 0 < A$
3		elrp	$⊢ A \in ℝ^{+} \leftrightarrow (A \in ℝ \land 0 < A)$
4	1 2 3	sylanbrc	$⊢ φ \to A \in ℝ^{+}$