Metamath Proof Explorer

Theorem ren0

Description: The set of reals is nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Assertion ren0 
|- RR =/= (/)

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 1 ne0ii 
 |-  RR =/= (/)