This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ren0

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

Ref Expression
Assertion ren0 ℝ ≠ ∅

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 1 ne0ii ⊢ ℝ ≠ ∅