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	⊢ ( 𝑁 ∈ ℕ0 ↔ 𝑁 ∈ ( ℤ≥ ‘ 0 ) )

Proof

Step	Hyp	Ref	Expression
1		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
2	1	eleq2i	⊢ ( 𝑁 ∈ ℕ0 ↔ 𝑁 ∈ ( ℤ≥ ‘ 0 ) )