Database
REAL AND COMPLEX NUMBERS
Order sets
Positive reals (as a subset of complex numbers)
rexrp
Next ⟩
rpaddcl
Metamath Proof Explorer
Ascii
Unicode
Theorem
rexrp
Description:
Quantification over positive reals.
(Contributed by
Mario Carneiro
, 21-May-2014)
Ref
Expression
Assertion
rexrp
⊢
∃
x
∈
ℝ
+
φ
↔
∃
x
∈
ℝ
0
<
x
∧
φ
Proof
Step
Hyp
Ref
Expression
1
elrp
⊢
x
∈
ℝ
+
↔
x
∈
ℝ
∧
0
<
x
2
1
anbi1i
⊢
x
∈
ℝ
+
∧
φ
↔
x
∈
ℝ
∧
0
<
x
∧
φ
3
anass
⊢
x
∈
ℝ
∧
0
<
x
∧
φ
↔
x
∈
ℝ
∧
0
<
x
∧
φ
4
2
3
bitri
⊢
x
∈
ℝ
+
∧
φ
↔
x
∈
ℝ
∧
0
<
x
∧
φ
5
4
rexbii2
⊢
∃
x
∈
ℝ
+
φ
↔
∃
x
∈
ℝ
0
<
x
∧
φ