Theorem nn0ex 9408

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 9403	. 2 |- NN0 = ( NN u. { 0 } )
2		nnex 9149	. . 3 |- NN e. _V
3		c0ex 8173	. . . 4 |- 0 e. _V
4	3	snex 4275	. . 3 |- { 0 } e. _V
5	2, 4	unex 4538	. 2 |- ( NN u. { 0 } ) e. _V
6	1, 5	eqeltri 2304	1 |- NN0 e. _V

Syntax hints:   e. wcel 2202   _Vcvv 2802   u. cun 3198   {csn 3669   0cc0 8032   NNcn 9143   NN0cn0 9402

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 2204  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-un 4530  ax-cnex 8123  ax-resscn 8124  ax-1cn 8125  ax-1re 8126  ax-icn 8127  ax-addcl 8128  ax-addrcl 8129  ax-mulcl 8130  ax-i2m1 8137

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-uni 3894  df-int 3929  df-inn 9144  df-n0 9403

This theorem is referenced by:  nn0ennn  10695  nnenom  10696  uzennn  10698  xnn0nnen  10699  wrdexg  11124  expcnvap0  12064  expcnvre  12065  expcnv  12066  geolim  12073  mertenslem2  12098  eftlub  12252  bitsfval  12504  bitsf  12508  1arith  12941  znnen  13020  psrval  14682  fnpsr  14683  psrbag  14685  psrbasg  14690  psrelbas  14691  psrplusgg  14694  psraddcl  14696  psr0cl  14697  psr0lid  14698  psrnegcl  14699  psrlinv  14700  psrgrp  14701  psr1clfi  14704  mplsubgfilemm  14714  mplsubgfilemcl  14715  plyval  15458  elply2  15461  plyf  15463  elplyr  15466  plyaddlem1  15473  plyaddlem  15475  plymullem  15476  plyco  15485  plycj  15487  plyrecj  15489  clwwlknonmpo  16281