Theorem nn0zrab

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

	Ref	Expression
Assertion	nn0zrab	$$⊢{\mathbb{N}}_0=\left\{x\in \mathbb{Z}|0\le x\right\}$$

Proof

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