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

Metamath Proof Explorer

Theorem elnn0uz

Description: A nonnegative integer expressed as a member an upper set of integers. (Contributed by NM, 6-Jun-2006)

Ref Expression
Assertion elnn0uz ⊢ N ∈ ℕ 0 ↔ N ∈ ℤ ≥ 0

Proof

Step Hyp Ref Expression
1 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
2 1 eleq2i ⊢ N ∈ ℕ 0 ↔ N ∈ ℤ ≥ 0