Theorem frexr

Description: A function taking real values, is a function taking extended real values. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypothesis	frexr.1	$$⊢\phi \to F:A⟶ℝ$$
Assertion	frexr	$$⊢\phi \to F:A⟶{ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		frexr.1	$$⊢\phi \to F:A⟶ℝ$$
2		ressxr	$$⊢ℝ\subseteq {ℝ}^{*}$$
3	2	a1i	$$⊢\phi \to ℝ\subseteq {ℝ}^{*}$$
4	1 3	fssd	$$⊢\phi \to F:A⟶{ℝ}^{*}$$