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\in {\mathbb{N}}_0\leftrightarrow N\in {\mathbb{Z}}_{\ge 0}$$

Proof

Step	Hyp	Ref	Expression
1		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
2	1	eleq2i	$$⊢N\in {\mathbb{N}}_0\leftrightarrow N\in {\mathbb{Z}}_{\ge 0}$$