**Description:** A positive real is a real. (Contributed by Mario Carneiro, 28-May-2016)

Ref | Expression | ||
---|---|---|---|

Hypothesis | rpred.1 | $${\u22a2}{\phi}\to {A}\in {\mathbb{R}}^{+}$$ | |

Assertion | rpred | $${\u22a2}{\phi}\to {A}\in \mathbb{R}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | rpred.1 | $${\u22a2}{\phi}\to {A}\in {\mathbb{R}}^{+}$$ | |

2 | rpssre | $${\u22a2}{\mathbb{R}}^{+}\subseteq \mathbb{R}$$ | |

3 | 2 1 | sseldi | $${\u22a2}{\phi}\to {A}\in \mathbb{R}$$ |