Theorem elnn0 9565

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 9564	. . 3 |- NN0 = ( NN u. { 0 } )
2	1	eleq2i 2305	. 2 |- ( A e. NN0 <-> A e. ( NN u. { 0 } ) )
3		elun 3370	. 2 |- ( A e. ( NN u. { 0 } ) <-> ( A e. NN \/ A e. { 0 } ) )
4		c0ex 8320	. . . 4 |- 0 e. _V
5	4	elsn2 3743	. . 3 |- ( A e. { 0 } <-> A = 0 )
6	5	orbi2i 774	. 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 ) )

This proof depends on syntax axioms:   <-> wb 105   \/ wo 720   = wceq 1402   e. wcel 2209   u. cun 3218   {csn 3709   0cc0 8179   NNcn 9304   NN0cn0 9563

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-ext 2220  ax-1cn 8272  ax-icn 8274  ax-addcl 8275  ax-mulcl 8277  ax-i2m1 8284

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-v 2823  df-un 3224  df-sn 3715  df-n0 9564

This theorem is used by:  0nn0  9578  nn0ge0  9588  nnnn0addcl  9593  nnm1nn0  9604  elnnnn0b  9607  elnn0z  9657  elznn0nn  9658  elznn0  9659  elznn  9660  nn0ind-raph  9763  nn0ledivnn  10168  expp1  10983  expnegap0  10984  expcllem  10987  nn0ltexp2  11147  facp1  11168  faclbnd  11179  faclbnd3  11181  bcn1  11196  bcval5  11201  hashnncl  11234  fz1f1o  12141  arisum  12265  arisum2  12266  fprodfac  12382  ef0lem  12427  nn0enne  12669  nn0o1gt2  12672  dfgcd2  12791  mulgcd  12793  eucalgf  12833  eucalginv  12834  prmdvdsexpr  12928  rpexp1i  12932  nn0gcdsq  12978  odzdvds  13024  pceq0  13101  fldivp1  13127  pockthg  13136  1arith  13146  4sqlem17  13186  4sqlem19  13188  mulgnn0gzsum  13931  mulgnn0p1  13936  mulgnn0subcl  13938  mulgneg  13943  mulgnn0z  13952  mulgnn0dir  13955  mulgnn0ass  13961  submmulg  13969  gsumvalfi  14152  znf1o  14986  dvexp2  15813  dvply1  15866  logfac  15995  birthdaylem2  16088  lgsdir  16154  lgsabs1  16158  lgseisenlem1  16189  2sqlem7  16240  clwwlknnn  16653