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	⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ) )

Proof

Step	Hyp	Ref	Expression
1		dfn2	⊢ ℕ = ( ℕ0 ∖ { 0 } )
2	1	eleq2i	⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( ℕ0 ∖ { 0 } ) )
3		eldifsn	⊢ ( 𝑁 ∈ ( ℕ0 ∖ { 0 } ) ↔ ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ) )
4	2 3	bitri	⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ) )