Theorem elnn0 9299

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 9298	. . 3 |- NN0 = ( NN u. { 0 } )
2	1	eleq2i 2272	. 2 |- ( A e. NN0 <-> A e. ( NN u. { 0 } ) )
3		elun 3314	. 2 |- ( A e. ( NN u. { 0 } ) <-> ( A e. NN \/ A e. { 0 } ) )
4		c0ex 8068	. . . 4 |- 0 e. _V
5	4	elsn2 3667	. . 3 |- ( A e. { 0 } <-> A = 0 )
6	5	orbi2i 764	. 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 710   = wceq 1373   e. wcel 2176   u. cun 3164   {csn 3633   0cc0 7927   NNcn 9038   NN0cn0 9297

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-1cn 8020  ax-icn 8022  ax-addcl 8023  ax-mulcl 8025  ax-i2m1 8032

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-n0 9298

This theorem is referenced by:  0nn0  9312  nn0ge0  9322  nnnn0addcl  9327  nnm1nn0  9338  elnnnn0b  9341  elnn0z  9387  elznn0nn  9388  elznn0  9389  elznn  9390  nn0ind-raph  9492  nn0ledivnn  9891  expp1  10693  expnegap0  10694  expcllem  10697  nn0ltexp2  10856  facp1  10877  faclbnd  10888  faclbnd3  10890  bcn1  10905  bcval5  10910  hashnncl  10942  fz1f1o  11719  arisum  11842  arisum2  11843  fprodfac  11959  ef0lem  12004  nn0enne  12246  nn0o1gt2  12249  dfgcd2  12368  mulgcd  12370  eucalgf  12410  eucalginv  12411  prmdvdsexpr  12505  rpexp1i  12509  nn0gcdsq  12555  odzdvds  12601  pceq0  12678  fldivp1  12704  pockthg  12713  1arith  12723  4sqlem17  12763  4sqlem19  12765  mulgnn0gsum  13497  mulgnn0p1  13502  mulgnn0subcl  13504  mulgneg  13509  mulgnn0z  13518  mulgnn0dir  13521  mulgnn0ass  13527  submmulg  13535  znf1o  14446  dvexp2  15217  dvply1  15270  lgsdir  15545  lgsabs1  15549  lgseisenlem1  15580  2sqlem7  15631