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 4086 | . 2 ⊢ ℕ ⊆ (ℕ ∪ {0}) | |
2 | df-n0 12091 | . 2 ⊢ ℕ0 = (ℕ ∪ {0}) | |
3 | 1, 2 | sseqtrri 3938 | 1 ⊢ ℕ ⊆ ℕ0 |
Colors of variables: wff setvar class |
Syntax hints: ∪ cun 3864 ⊆ wss 3866 {csn 4541 0cc0 10729 ℕcn 11830 ℕ0cn0 12090 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3410 df-un 3871 df-in 3873 df-ss 3883 df-n0 12091 |
This theorem is referenced by: nnnn0 12097 nnnn0d 12150 nthruz 15814 oddge22np1 15910 bitsfzolem 15993 lcmfval 16178 ramub1 16581 ramcl 16582 ply1divex 25034 pserdvlem2 25320 2sqreunnlem1 26330 2sqreunnlem2 26336 fsum2dsub 32299 breprexplemc 32324 breprexpnat 32326 knoppndvlem18 34446 hbtlem5 40656 brfvtrcld 41006 corcltrcl 41024 fourierdlem50 43372 fourierdlem102 43424 fourierdlem114 43436 fmtnoinf 44661 fmtnofac2 44694 |
Copyright terms: Public domain | W3C validator |