Metamath Proof Explorer


Theorem nnn0

Description: The set of positive integers is nonempty. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Assertion nnn0 ℕ ≠ ∅

Proof

Step Hyp Ref Expression
1 1nn 1 ∈ ℕ
2 1 ne0ii ℕ ≠ ∅