![]() |
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 11750 | . 2 class ℕ0 | |
2 | cn 11491 | . . 3 class ℕ | |
3 | cc0 10388 | . . . 4 class 0 | |
4 | 3 | csn 4476 | . . 3 class {0} |
5 | 2, 4 | cun 3861 | . 2 class (ℕ ∪ {0}) |
6 | 1, 5 | wceq 1522 | 1 wff ℕ0 = (ℕ ∪ {0}) |
Colors of variables: wff setvar class |
This definition is referenced by: elnn0 11752 nnssnn0 11753 nn0ssre 11754 nn0sscn 11755 nn0ex 11756 dfn2 11763 nn0addcl 11785 nn0mulcl 11786 nn0ssz 11857 dvdsprmpweqnn 16055 cply1coe0bi 20156 m2cpminvid2lem 21051 pmatcollpw3fi1 21085 dfrtrcl4 39593 corcltrcl 39594 cotrclrcl 39597 |
Copyright terms: Public domain | W3C validator |