Theorem nnzrab

Description: Positive integers expressed as a subset of integers. (Contributed by NM, 3-Oct-2004)

	Ref	Expression
Assertion	nnzrab	$$⊢\mathbb{N}=\left\{x\in \mathbb{Z}|1\le x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		elnnz1	$$⊢x\in \mathbb{N}\leftrightarrow \left(x\in \mathbb{Z}\wedge 1\le x\right)$$
2	1	eqabi	$$⊢\mathbb{N}=\left\{x|\left(x\in \mathbb{Z}\wedge 1\le x\right)\right\}$$
3		df-rab	$$⊢\left\{x\in \mathbb{Z}|1\le x\right\}=\left\{x|\left(x\in \mathbb{Z}\wedge 1\le x\right)\right\}$$
4	2 3	eqtr4i	$$⊢\mathbb{N}=\left\{x\in \mathbb{Z}|1\le x\right\}$$