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

Metamath Proof Explorer

Theorem elnn0

Description: Nonnegative integers expressed in terms of naturals and zero. (Contributed by Raph Levien, 10-Dec-2002)

Ref Expression
Assertion elnn0 ⊢ A ∈ ℕ 0 ↔ A ∈ ℕ ∨ A = 0

Proof

Step Hyp Ref Expression
1 df-n0 ⊢ ℕ 0 = ℕ ∪ 0
2 1 eleq2i ⊢ A ∈ ℕ 0 ↔ A ∈ ℕ ∪ 0
3 elun ⊢ A ∈ ℕ ∪ 0 ↔ A ∈ ℕ ∨ A ∈ 0
4 c0ex ⊢ 0 ∈ V
5 4 elsn2 ⊢ A ∈ 0 ↔ A = 0
6 5 orbi2i ⊢ A ∈ ℕ ∨ A ∈ 0 ↔ A ∈ ℕ ∨ A = 0
7 2 3 6 3bitri ⊢ A ∈ ℕ 0 ↔ A ∈ ℕ ∨ A = 0