![]() |
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 12523 | . 2 class ℕ0 | |
2 | cn 12263 | . . 3 class ℕ | |
3 | cc0 11152 | . . . 4 class 0 | |
4 | 3 | csn 4630 | . . 3 class {0} |
5 | 2, 4 | cun 3960 | . 2 class (ℕ ∪ {0}) |
6 | 1, 5 | wceq 1536 | 1 wff ℕ0 = (ℕ ∪ {0}) |
Colors of variables: wff setvar class |
This definition is referenced by: elnn0 12525 nnssnn0 12526 nn0ssre 12527 nn0sscn 12528 nn0ex 12529 dfn2 12536 nn0addcl 12558 nn0mulcl 12559 nn0ssz 12633 dvdsprmpweqnn 16918 cply1coe0bi 22321 m2cpminvid2lem 22775 pmatcollpw3fi1 22809 dfrtrcl4 43727 corcltrcl 43728 cotrclrcl 43731 |
Copyright terms: Public domain | W3C validator |