![]() |
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 12524 | . 2 class ℕ0 | |
2 | cn 12264 | . . 3 class ℕ | |
3 | cc0 11158 | . . . 4 class 0 | |
4 | 3 | csn 4633 | . . 3 class {0} |
5 | 2, 4 | cun 3945 | . 2 class (ℕ ∪ {0}) |
6 | 1, 5 | wceq 1534 | 1 wff ℕ0 = (ℕ ∪ {0}) |
Colors of variables: wff setvar class |
This definition is referenced by: elnn0 12526 nnssnn0 12527 nn0ssre 12528 nn0sscn 12529 nn0ex 12530 dfn2 12537 nn0addcl 12559 nn0mulcl 12560 nn0ssz 12633 dvdsprmpweqnn 16887 cply1coe0bi 22293 m2cpminvid2lem 22747 pmatcollpw3fi1 22781 dfrtrcl4 43405 corcltrcl 43406 cotrclrcl 43409 |
Copyright terms: Public domain | W3C validator |