This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ ℕ = ℕ_{0} ∖ \{0\}$

Proof

Step	Hyp	Ref	Expression
1		df-n0	$⊢ ℕ_{0} = ℕ \cup \{0\}$
2	1	difeq1i	$⊢ ℕ_{0} ∖ \{0\} = (ℕ \cup \{0\}) ∖ \{0\}$
3		difun2	$⊢ (ℕ \cup \{0\}) ∖ \{0\} = ℕ ∖ \{0\}$
4		0nnn	$⊢ \neg 0 \in ℕ$
5		difsn	$⊢ \neg 0 \in ℕ \to ℕ ∖ \{0\} = ℕ$
6	4 5	ax-mp	$⊢ ℕ ∖ \{0\} = ℕ$
7	2 3 6	3eqtrri	$⊢ ℕ = ℕ_{0} ∖ \{0\}$