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