![]() |
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 12371 | . 2 class ℕ0 | |
2 | cn 12111 | . . 3 class ℕ | |
3 | cc0 11009 | . . . 4 class 0 | |
4 | 3 | csn 4584 | . . 3 class {0} |
5 | 2, 4 | cun 3906 | . 2 class (ℕ ∪ {0}) |
6 | 1, 5 | wceq 1541 | 1 wff ℕ0 = (ℕ ∪ {0}) |
Colors of variables: wff setvar class |
This definition is referenced by: elnn0 12373 nnssnn0 12374 nn0ssre 12375 nn0sscn 12376 nn0ex 12377 dfn2 12384 nn0addcl 12406 nn0mulcl 12407 nn0ssz 12480 dvdsprmpweqnn 16717 cply1coe0bi 21623 m2cpminvid2lem 22055 pmatcollpw3fi1 22089 dfrtrcl4 41921 corcltrcl 41922 cotrclrcl 41925 |
Copyright terms: Public domain | W3C validator |