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 = ( ℕ ∪ { 0 } )
2	1	difeq1i	⊢ ( ℕ0 ∖ { 0 } ) = ( ( ℕ ∪ { 0 } ) ∖ { 0 } )
3		difun2	⊢ ( ( ℕ ∪ { 0 } ) ∖ { 0 } ) = ( ℕ ∖ { 0 } )
4		0nnn	⊢ ¬ 0 ∈ ℕ
5		difsn	⊢ ( ¬ 0 ∈ ℕ → ( ℕ ∖ { 0 } ) = ℕ )
6	4 5	ax-mp	⊢ ( ℕ ∖ { 0 } ) = ℕ
7	2 3 6	3eqtrri	⊢ ℕ = ( ℕ0 ∖ { 0 } )