Theorem elnn0 9519

Description: Nonnegative integers expressed in terms of naturals and zero. (Contributed by Raph Levien, 10-Dec-2002.)

Assertion

Ref	Expression
elnn0	|- ( A e. NN0 <-> ( A e. NN \/ A = 0 ) )

Proof of Theorem elnn0

Step	Hyp	Ref	Expression
1		df-n0 9518	. . 3 |- NN0 = ( NN u. { 0 } )
2	1	eleq2i 2301	. 2 |- ( A e. NN0 <-> A e. ( NN u. { 0 } ) )
3		elun 3364	. 2 |- ( A e. ( NN u. { 0 } ) <-> ( A e. NN \/ A e. { 0 } ) )
4		c0ex 8285	. . . 4 |- 0 e. _V
5	4	elsn2 3729	. . 3 |- ( A e. { 0 } <-> A = 0 )
6	5	orbi2i 770	. 2 |- ( ( A e. NN \/ A e. { 0 } ) <-> ( A e. NN \/ A = 0 ) )
7	2, 3, 6	3bitri 206	1 |- ( A e. NN0 <-> ( A e. NN \/ A = 0 ) )

Syntax hints:   <-> wb 105   \/ wo 716   = wceq 1398   e. wcel 2205   u. cun 3212   {csn 3695   0cc0 8144   NNcn 9258   NN0cn0 9517

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-ext 2216  ax-1cn 8237  ax-icn 8239  ax-addcl 8240  ax-mulcl 8242  ax-i2m1 8249

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-v 2817  df-un 3218  df-sn 3701  df-n0 9518

This theorem is referenced by:  0nn0  9532  nn0ge0  9542  nnnn0addcl  9547  nnm1nn0  9558  elnnnn0b  9561  elnn0z  9611  elznn0nn  9612  elznn0  9613  elznn  9614  nn0ind-raph  9717  nn0ledivnn  10122  expp1  10936  expnegap0  10937  expcllem  10940  nn0ltexp2  11100  facp1  11121  faclbnd  11132  faclbnd3  11134  bcn1  11149  bcval5  11154  hashnncl  11187  fz1f1o  12090  arisum  12214  arisum2  12215  fprodfac  12331  ef0lem  12376  nn0enne  12618  nn0o1gt2  12621  dfgcd2  12740  mulgcd  12742  eucalgf  12782  eucalginv  12783  prmdvdsexpr  12877  rpexp1i  12881  nn0gcdsq  12927  odzdvds  12973  pceq0  13050  fldivp1  13076  pockthg  13085  1arith  13095  4sqlem17  13135  4sqlem19  13137  mulgnn0gsum  13886  mulgnn0p1  13891  mulgnn0subcl  13893  mulgneg  13898  mulgnn0z  13907  mulgnn0dir  13910  mulgnn0ass  13916  submmulg  13924  gfsumval  14107  znf1o  14930  dvexp2  15708  dvply1  15761  lgsdir  16039  lgsabs1  16043  lgseisenlem1  16074  2sqlem7  16125  clwwlknnn  16538