Metamath Proof Explorer


Theorem rexri

Description: A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypothesis rexri.1 𝐴 ∈ ℝ
Assertion rexri 𝐴 ∈ ℝ*

Proof

Step Hyp Ref Expression
1 rexri.1 𝐴 ∈ ℝ
2 rexr ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
3 1 2 ax-mp 𝐴 ∈ ℝ*