This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database REAL AND COMPLEX NUMBERS Integer sets Nonnegative integers (as a subset of complex numbers) 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 } )