Theorem nn0ex 9246

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 9241	. 2 |- NN0 = ( NN u. { 0 } )
2		nnex 8988	. . 3 |- NN e. _V
3		c0ex 8013	. . . 4 |- 0 e. _V
4	3	snex 4214	. . 3 |- { 0 } e. _V
5	2, 4	unex 4472	. 2 |- ( NN u. { 0 } ) e. _V
6	1, 5	eqeltri 2266	1 |- NN0 e. _V

Syntax hints:   e. wcel 2164   _Vcvv 2760   u. cun 3151   {csn 3618   0cc0 7872   NNcn 8982   NN0cn0 9240

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238  ax-un 4464  ax-cnex 7963  ax-resscn 7964  ax-1cn 7965  ax-1re 7966  ax-icn 7967  ax-addcl 7968  ax-addrcl 7969  ax-mulcl 7970  ax-i2m1 7977

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-uni 3836  df-int 3871  df-inn 8983  df-n0 9241

This theorem is referenced by:  nn0ennn  10504  nnenom  10505  uzennn  10507  xnn0nnen  10508  wrdexg  10925  expcnvap0  11645  expcnvre  11646  expcnv  11647  geolim  11654  mertenslem2  11679  eftlub  11833  1arith  12505  znnen  12555  psrval  14152  fnpsr  14153  psrbag  14155  psrbasg  14159  psrelbas  14160  psrplusgg  14162  psraddcl  14164  plyval  14878  elply2  14881  plyf  14883  elplyr  14886  plyaddlem1  14893  plyaddlem  14895  plymullem  14896