Description: A nonnegative integer expressed as a member an upper set of integers. (Contributed by NM, 6-Jun-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | elnn0uz | ⊢ ( 𝑁 ∈ ℕ_{0} ↔ 𝑁 ∈ ( ℤ_{≥} ‘ 0 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nn0uz | ⊢ ℕ_{0} = ( ℤ_{≥} ‘ 0 ) | |
2 | 1 | eleq2i | ⊢ ( 𝑁 ∈ ℕ_{0} ↔ 𝑁 ∈ ( ℤ_{≥} ‘ 0 ) ) |