Theorem dfn2

Description: The set of positive integers defined in terms of nonnegative integers. (Contributed by NM, 23-Sep-2007) (Proof shortened by Mario Carneiro, 13-Feb-2013)

	Ref	Expression
Assertion	dfn2	$$⊢\mathbb{N}={\mathbb{N}}_0\setminus \left\{0\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-n0	$$⊢{\mathbb{N}}_0=\mathbb{N}\cup \left\{0\right\}$$
2	1	difeq1i	$$⊢{\mathbb{N}}_0\setminus \left\{0\right\}=\left(\mathbb{N}\cup \left\{0\right\}\right)\setminus \left\{0\right\}$$
3		difun2	$$⊢\left(\mathbb{N}\cup \left\{0\right\}\right)\setminus \left\{0\right\}=\mathbb{N}\setminus \left\{0\right\}$$
4		0nnn	$$⊢\neg 0\in \mathbb{N}$$
5		difsn	$$⊢\neg 0\in \mathbb{N}\to \mathbb{N}\setminus \left\{0\right\}=\mathbb{N}$$
6	4 5	ax-mp	$$⊢\mathbb{N}\setminus \left\{0\right\}=\mathbb{N}$$
7	2 3 6	3eqtrri	$$⊢\mathbb{N}={\mathbb{N}}_0\setminus \left\{0\right\}$$