Metamath Proof Explorer
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* ) |