![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nnssnn0 | Structured version Visualization version GIF version |
Description: Positive naturals are a subset of nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002.) |
Ref | Expression |
---|---|
nnssnn0 | ⊢ ℕ ⊆ ℕ0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssun1 4171 | . 2 ⊢ ℕ ⊆ (ℕ ∪ {0}) | |
2 | df-n0 12469 | . 2 ⊢ ℕ0 = (ℕ ∪ {0}) | |
3 | 1, 2 | sseqtrri 4018 | 1 ⊢ ℕ ⊆ ℕ0 |
Colors of variables: wff setvar class |
Syntax hints: ∪ cun 3945 ⊆ wss 3947 {csn 4627 0cc0 11106 ℕcn 12208 ℕ0cn0 12468 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-un 3952 df-in 3954 df-ss 3964 df-n0 12469 |
This theorem is referenced by: nnnn0 12475 nnnn0d 12528 nthruz 16192 oddge22np1 16288 bitsfzolem 16371 lcmfval 16554 ramub1 16957 ramcl 16958 ply1divex 25636 pserdvlem2 25922 2sqreunnlem1 26932 2sqreunnlem2 26938 fsum2dsub 33557 breprexplemc 33582 breprexpnat 33584 knoppndvlem18 35343 hbtlem5 41803 brfvtrcld 42405 corcltrcl 42423 fourierdlem50 44807 fourierdlem102 44859 fourierdlem114 44871 fmtnoinf 46139 fmtnofac2 46172 |
Copyright terms: Public domain | W3C validator |