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

Metamath Proof Explorer

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 ⊢ N ∈ ℕ ↔ N ∈ ℕ 0 ∧ N ≠ 0

Proof

Step Hyp Ref Expression
1 dfn2 ⊢ ℕ = ℕ 0 ∖ 0
2 1 eleq2i ⊢ N ∈ ℕ ↔ N ∈ ℕ 0 ∖ 0
3 eldifsn ⊢ N ∈ ℕ 0 ∖ 0 ↔ N ∈ ℕ 0 ∧ N ≠ 0
4 2 3 bitri ⊢ N ∈ ℕ ↔ N ∈ ℕ 0 ∧ N ≠ 0