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

Metamath Proof Explorer

Theorem rexrp

Description: Quantification over positive reals. (Contributed by Mario Carneiro, 21-May-2014)

		Ref	Expression
	Assertion	rexrp	$⊢ \exists x \in ℝ^{+} φ \leftrightarrow \exists x \in ℝ (0 < x \land φ)$

Step	Hyp	Ref	Expression
1		elrp	$⊢ x \in ℝ^{+} \leftrightarrow (x \in ℝ \land 0 < x)$
2	1	anbi1i	$⊢ (x \in ℝ^{+} \land φ) \leftrightarrow ((x \in ℝ \land 0 < x) \land φ)$
3		anass	$⊢ ((x \in ℝ \land 0 < x) \land φ) \leftrightarrow (x \in ℝ \land (0 < x \land φ))$
4	2 3	bitri	$⊢ (x \in ℝ^{+} \land φ) \leftrightarrow (x \in ℝ \land (0 < x \land φ))$
5	4	rexbii2	$⊢ \exists x \in ℝ^{+} φ \leftrightarrow \exists x \in ℝ (0 < x \land φ)$