Theorem elnnuz

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

	Ref	Expression
Assertion	elnnuz	$$⊢N\in \mathbb{N}\leftrightarrow N\in {\mathbb{Z}}_{\ge 1}$$

Proof

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