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

Metamath Proof Explorer

Theorem ralrp

Description: Quantification over positive reals. (Contributed by NM, 12-Feb-2008)

		Ref	Expression
	Assertion	ralrp	$⊢ \forall x \in ℝ^{+} φ \leftrightarrow \forall x \in ℝ (0 < x \to φ)$

Step	Hyp	Ref	Expression
1		elrp	$⊢ x \in ℝ^{+} \leftrightarrow (x \in ℝ \land 0 < x)$
2	1	imbi1i	$⊢ (x \in ℝ^{+} \to φ) \leftrightarrow ((x \in ℝ \land 0 < x) \to φ)$
3		impexp	$⊢ ((x \in ℝ \land 0 < x) \to φ) \leftrightarrow (x \in ℝ \to (0 < x \to φ))$
4	2 3	bitri	$⊢ (x \in ℝ^{+} \to φ) \leftrightarrow (x \in ℝ \to (0 < x \to φ))$
5	4	ralbii2	$⊢ \forall x \in ℝ^{+} φ \leftrightarrow \forall x \in ℝ (0 < x \to φ)$