Theorem nn0ex 9413

Description: The set of nonnegative integers exists. (Contributed by NM, 18-Jul-2004.)

Assertion

Ref	Expression
nn0ex	|- NN0 e. _V

Proof of Theorem nn0ex

Step	Hyp	Ref	Expression
1		df-n0 9408	. 2 |- NN0 = ( NN u. { 0 } )
2		nnex 9154	. . 3 |- NN e. _V
3		c0ex 8178	. . . 4 |- 0 e. _V
4	3	snex 4277	. . 3 |- { 0 } e. _V
5	2, 4	unex 4540	. 2 |- ( NN u. { 0 } ) e. _V
6	1, 5	eqeltri 2303	1 |- NN0 e. _V

Syntax hints:   e. wcel 2201   _Vcvv 2801   u. cun 3197   {csn 3670   0cc0 8037   NNcn 9148   NN0cn0 9407

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2203  ax-14 2204  ax-ext 2212  ax-sep 4208  ax-pow 4266  ax-pr 4301  ax-un 4532  ax-cnex 8128  ax-resscn 8129  ax-1cn 8130  ax-1re 8131  ax-icn 8132  ax-addcl 8133  ax-addrcl 8134  ax-mulcl 8135  ax-i2m1 8142

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ral 2514  df-rex 2515  df-v 2803  df-un 3203  df-in 3205  df-ss 3212  df-pw 3655  df-sn 3676  df-pr 3677  df-uni 3895  df-int 3930  df-inn 9149  df-n0 9408

This theorem is referenced by:  nn0ennn  10701  nnenom  10702  uzennn  10704  xnn0nnen  10705  wrdexg  11133  expcnvap0  12086  expcnvre  12087  expcnv  12088  geolim  12095  mertenslem2  12120  eftlub  12274  bitsfval  12526  bitsf  12530  1arith  12963  znnen  13042  psrval  14704  fnpsr  14705  psrbag  14707  psrbasg  14717  psrelbas  14718  psrplusgg  14721  psraddcl  14723  psr0cl  14724  psr0lid  14725  psrnegcl  14726  psrlinv  14727  psrgrp  14728  psr1clfi  14731  mplsubgfilemm  14741  mplsubgfilemcl  14742  plyval  15485  elply2  15488  plyf  15490  elplyr  15493  plyaddlem1  15500  plyaddlem  15502  plymullem  15503  plyco  15512  plycj  15514  plyrecj  15516  clwwlknonmpo  16308  depindlem1  16386  depindlem2  16387