Metamath Proof Explorer


Theorem ssrexr

Description: A subset of the reals is a subset of the extended reals. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypothesis ssrexr.1
|- ( ph -> A C_ RR )
Assertion ssrexr
|- ( ph -> A C_ RR* )

Proof

Step Hyp Ref Expression
1 ssrexr.1
 |-  ( ph -> A C_ RR )
2 ressxr
 |-  RR C_ RR*
3 1 2 sstrdi
 |-  ( ph -> A C_ RR* )