This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
Assertion ssrexr ( 𝜑 → 𝐴 ⊆ ℝ* )

Proof

Step Hyp Ref Expression
1 ssrexr.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2 ressxr ⊢ ℝ ⊆ ℝ*
3 1 2 sstrdi ⊢ ( 𝜑 → 𝐴 ⊆ ℝ* )