![]() |
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 12469 | . 2 class ℕ0 | |
2 | cn 12209 | . . 3 class ℕ | |
3 | cc0 11107 | . . . 4 class 0 | |
4 | 3 | csn 4628 | . . 3 class {0} |
5 | 2, 4 | cun 3946 | . 2 class (ℕ ∪ {0}) |
6 | 1, 5 | wceq 1542 | 1 wff ℕ0 = (ℕ ∪ {0}) |
Colors of variables: wff setvar class |
This definition is referenced by: elnn0 12471 nnssnn0 12472 nn0ssre 12473 nn0sscn 12474 nn0ex 12475 dfn2 12482 nn0addcl 12504 nn0mulcl 12505 nn0ssz 12578 dvdsprmpweqnn 16815 cply1coe0bi 21816 m2cpminvid2lem 22248 pmatcollpw3fi1 22282 dfrtrcl4 42475 corcltrcl 42476 cotrclrcl 42479 |
Copyright terms: Public domain | W3C validator |