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 
|- A e. RR
Assertion rexri 
|- A e. RR*

Proof

Step Hyp Ref Expression
1 rexri.1 
 |-  A e. RR
2 rexr 
 |-  ( A e. RR -> A e. RR* )
3 1 2 ax-mp 
 |-  A e. RR*