Theorem nn0ex 9581

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 9576	. 2 |- NN0 = ( NN u. { 0 } )
2		nnex 9320	. . 3 |- NN e. _V
3		c0ex 8327	. . . 4 |- 0 e. _V
4	3	snex 4324	. . 3 |- { 0 } e. _V
5	2, 4	unex 4589	. 2 |- ( NN u. { 0 } ) e. _V
6	1, 5	eqeltri 2311	1 |- NN0 e. _V

This proof depends on syntax axioms:   e. wcel 2209   _Vcvv 2821   u. cun 3218   {csn 3709   0cc0 8186   NNcn 9314   NN0cn0 9575

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-pow 4313  ax-pr 4348  ax-un 4580  ax-cnex 8277  ax-resscn 8278  ax-1cn 8279  ax-1re 8280  ax-icn 8281  ax-addcl 8282  ax-addrcl 8283  ax-mulcl 8284  ax-i2m1 8291

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-uni 3936  df-int 3971  df-inn 9315  df-n0 9576

This theorem is used by:  nn0ennn  10892  nnenom  10893  uzennn  10895  xnn0nnen  10896  wrdexg  11338  expcnvap0  12295  expcnvre  12296  expcnv  12297  geolim  12304  mertenslem2  12329  eftlub  12483  bitsfval  12735  bitsf  12739  1arith  13176  znnen  13348  psrval  15162  fnpsr  15163  psrbag  15165  snifpsrbagfi  15170  psrbagaddclfi  15175  psrbaglefifi  15177  psrbasg  15183  psrelbas  15184  psrplusgg  15187  psraddcl  15189  psrmulrg  15191  psrmulfval  15192  psrmulclfilem  15194  psr0cl  15196  psr0lid  15197  psrnegcl  15198  psrlinv  15199  psrgrp  15200  psr1clfi  15203  psrdifi  15207  psrdirfi  15208  mvrval  15211  mvrffi  15214  mplsubgfilemm  15226  mplsubgfilemcl  15227  plyval  15970  elply2  15973  plyf  15975  elplyr  15978  plyaddlem1  15985  plyaddlem  15987  plymullem  15988  plyco  15997  plycj  15999  plyrecj  16001  clwwlknonmpo  16886  depindlem1  16964  depindlem2  16965