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 11886 | . 2 class ℕ0 | |
2 | cn 11627 | . . 3 class ℕ | |
3 | cc0 10526 | . . . 4 class 0 | |
4 | 3 | csn 4559 | . . 3 class {0} |
5 | 2, 4 | cun 3933 | . 2 class (ℕ ∪ {0}) |
6 | 1, 5 | wceq 1528 | 1 wff ℕ0 = (ℕ ∪ {0}) |
Colors of variables: wff setvar class |
This definition is referenced by: elnn0 11888 nnssnn0 11889 nn0ssre 11890 nn0sscn 11891 nn0ex 11892 dfn2 11899 nn0addcl 11921 nn0mulcl 11922 nn0ssz 11992 dvdsprmpweqnn 16211 cply1coe0bi 20398 m2cpminvid2lem 21292 pmatcollpw3fi1 21326 dfrtrcl4 39963 corcltrcl 39964 cotrclrcl 39967 |
Copyright terms: Public domain | W3C validator |