Metamath Proof Explorer


Theorem rpex

Description: The positive reals form a set. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Assertion rpex + ∈ V

Proof

Step Hyp Ref Expression
1 reex ℝ ∈ V
2 rpssre + ⊆ ℝ
3 1 2 ssexi + ∈ V