Description: A standard real is an extended real. (Contributed by NM, 14-Oct-2005)
Ref | Expression | ||
---|---|---|---|
Assertion | rexr | $${\u22a2}{A}\in \mathbb{R}\to {A}\in {\mathbb{R}}^{*}$$ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ressxr | $${\u22a2}\mathbb{R}\subseteq {\mathbb{R}}^{*}$$ | |
2 | 1 | sseli | $${\u22a2}{A}\in \mathbb{R}\to {A}\in {\mathbb{R}}^{*}$$ |