Theorem nn0ex 9507

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 9502	. 2 |- NN0 = ( NN u. { 0 } )
2		nnex 9248	. . 3 |- NN e. _V
3		c0ex 8273	. . . 4 |- 0 e. _V
4	3	snex 4300	. . 3 |- { 0 } e. _V
5	2, 4	unex 4564	. 2 |- ( NN u. { 0 } ) e. _V
6	1, 5	eqeltri 2307	1 |- NN0 e. _V

Syntax hints:   e. wcel 2205   _Vcvv 2815   u. cun 3211   {csn 3691   0cc0 8132   NNcn 9242   NN0cn0 9501

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2207  ax-14 2208  ax-ext 2216  ax-sep 4230  ax-pow 4289  ax-pr 4324  ax-un 4556  ax-cnex 8223  ax-resscn 8224  ax-1cn 8225  ax-1re 8226  ax-icn 8227  ax-addcl 8228  ax-addrcl 8229  ax-mulcl 8230  ax-i2m1 8237

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-un 3217  df-in 3219  df-ss 3226  df-pw 3673  df-sn 3697  df-pr 3698  df-uni 3917  df-int 3952  df-inn 9243  df-n0 9502

This theorem is referenced by:  nn0ennn  10802  nnenom  10803  uzennn  10805  xnn0nnen  10806  wrdexg  11243  expcnvap0  12196  expcnvre  12197  expcnv  12198  geolim  12205  mertenslem2  12230  eftlub  12384  bitsfval  12636  bitsf  12640  1arith  13073  znnen  13170  psrval  14863  fnpsr  14864  psrbag  14866  psrbagaddclfi  14874  psrbasg  14878  psrelbas  14879  psrplusgg  14882  psraddcl  14884  psr0cl  14885  psr0lid  14886  psrnegcl  14887  psrlinv  14888  psrgrp  14889  psr1clfi  14892  mplsubgfilemm  14902  mplsubgfilemcl  14903  plyval  15646  elply2  15649  plyf  15651  elplyr  15654  plyaddlem1  15661  plyaddlem  15663  plymullem  15664  plyco  15673  plycj  15675  plyrecj  15677  clwwlknonmpo  16472  depindlem1  16550  depindlem2  16551