| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-n0 | Structured version Visualization version GIF version | ||
| Description: Define the set of nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002.) |
| Ref | Expression |
|---|---|
| df-n0 | ⊢ ℕ0 = (ℕ ∪ {0}) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cn0 12526 | . 2 class ℕ0 | |
| 2 | cn 12266 | . . 3 class ℕ | |
| 3 | cc0 11155 | . . . 4 class 0 | |
| 4 | 3 | csn 4626 | . . 3 class {0} |
| 5 | 2, 4 | cun 3949 | . 2 class (ℕ ∪ {0}) |
| 6 | 1, 5 | wceq 1540 | 1 wff ℕ0 = (ℕ ∪ {0}) |
| Colors of variables: wff setvar class |
| This definition is referenced by: elnn0 12528 nnssnn0 12529 nn0ssre 12530 nn0sscn 12531 nn0ex 12532 dfn2 12539 nn0addcl 12561 nn0mulcl 12562 nn0ssz 12636 dvdsprmpweqnn 16923 cply1coe0bi 22306 m2cpminvid2lem 22760 pmatcollpw3fi1 22794 dfrtrcl4 43751 corcltrcl 43752 cotrclrcl 43755 |
| Copyright terms: Public domain | W3C validator |