Theorem elnnne0

Description: The positive integer property expressed in terms of difference from zero. (Contributed by Stefan O'Rear, 12-Sep-2015)

	Ref	Expression
Assertion	elnnne0	$$⊢N\in \mathbb{N}\leftrightarrow \left(N\in {\mathbb{N}}_0\wedge N\ne 0\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfn2	$$⊢\mathbb{N}={\mathbb{N}}_0\setminus \left\{0\right\}$$
2	1	eleq2i	$$⊢N\in \mathbb{N}\leftrightarrow N\in \left({\mathbb{N}}_0\setminus \left\{0\right\}\right)$$
3		eldifsn	$$⊢N\in \left({\mathbb{N}}_0\setminus \left\{0\right\}\right)\leftrightarrow \left(N\in {\mathbb{N}}_0\wedge N\ne 0\right)$$
4	2 3	bitri	$$⊢N\in \mathbb{N}\leftrightarrow \left(N\in {\mathbb{N}}_0\wedge N\ne 0\right)$$