Metamath Proof Explorer

Theorem rpex

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

Ref Expression
Assertion rpex 
|- RR+ e. _V

Proof

Step Hyp Ref Expression
1 reex 
 |-  RR e. _V
2 rpssre 
 |-  RR+ C_ RR
3 1 2 ssexi 
 |-  RR+ e. _V