Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rpre | Structured version Visualization version GIF version |
Description: A positive real is a real. (Contributed by NM, 27-Oct-2007.) |
Ref | Expression |
---|---|
rpre | ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rp 11833 | . . 3 ⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥} | |
2 | ssrab2 3687 | . . 3 ⊢ {𝑥 ∈ ℝ ∣ 0 < 𝑥} ⊆ ℝ | |
3 | 1, 2 | eqsstri 3635 | . 2 ⊢ ℝ+ ⊆ ℝ |
4 | 3 | sseli 3599 | 1 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ) |
Copyright terms: Public domain | W3C validator |