Description: Nonnegative integers expressed in terms of naturals and zero. (Contributed by Raph Levien, 10-Dec-2002)
Ref | Expression | ||
---|---|---|---|
Assertion | elnn0 | ⊢ ( 𝐴 ∈ ℕ_{0} ↔ ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-n0 | ⊢ ℕ_{0} = ( ℕ ∪ { 0 } ) | |
2 | 1 | eleq2i | ⊢ ( 𝐴 ∈ ℕ_{0} ↔ 𝐴 ∈ ( ℕ ∪ { 0 } ) ) |
3 | elun | ⊢ ( 𝐴 ∈ ( ℕ ∪ { 0 } ) ↔ ( 𝐴 ∈ ℕ ∨ 𝐴 ∈ { 0 } ) ) | |
4 | c0ex | ⊢ 0 ∈ V | |
5 | 4 | elsn2 | ⊢ ( 𝐴 ∈ { 0 } ↔ 𝐴 = 0 ) |
6 | 5 | orbi2i | ⊢ ( ( 𝐴 ∈ ℕ ∨ 𝐴 ∈ { 0 } ) ↔ ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) ) |
7 | 2 3 6 | 3bitri | ⊢ ( 𝐴 ∈ ℕ_{0} ↔ ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) ) |