| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > nn0ex | Structured version Visualization version GIF version | ||
| Description: The set of nonnegative integers exists. (Contributed by NM, 18-Jul-2004.) |
| Ref | Expression |
|---|---|
| nn0ex | ⊢ ℕ0 ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-n0 12527 | . 2 ⊢ ℕ0 = (ℕ ∪ {0}) | |
| 2 | nnex 12272 | . . 3 ⊢ ℕ ∈ V | |
| 3 | snex 5436 | . . 3 ⊢ {0} ∈ V | |
| 4 | 2, 3 | unex 7764 | . 2 ⊢ (ℕ ∪ {0}) ∈ V |
| 5 | 1, 4 | eqeltri 2837 | 1 ⊢ ℕ0 ∈ V |
| Copyright terms: Public domain | W3C validator |