Theorem elnn0 9178

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 9177	. . 3 |- NN0 = ( NN u. { 0 } )
2	1	eleq2i 2244	. 2 |- ( A e. NN0 <-> A e. ( NN u. { 0 } ) )
3		elun 3277	. 2 |- ( A e. ( NN u. { 0 } ) <-> ( A e. NN \/ A e. { 0 } ) )
4		c0ex 7951	. . . 4 |- 0 e. _V
5	4	elsn2 3627	. . 3 |- ( A e. { 0 } <-> A = 0 )
6	5	orbi2i 762	. 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 708   = wceq 1353   e. wcel 2148   u. cun 3128   {csn 3593   0cc0 7811   NNcn 8919   NN0cn0 9176

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-1cn 7904  ax-icn 7906  ax-addcl 7907  ax-mulcl 7909  ax-i2m1 7916

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-un 3134  df-sn 3599  df-n0 9177

This theorem is referenced by:  0nn0  9191  nn0ge0  9201  nnnn0addcl  9206  nnm1nn0  9217  elnnnn0b  9220  elnn0z  9266  elznn0nn  9267  elznn0  9268  elznn  9269  nn0ind-raph  9370  nn0ledivnn  9767  expp1  10527  expnegap0  10528  expcllem  10531  nn0ltexp2  10689  facp1  10710  faclbnd  10721  faclbnd3  10723  bcn1  10738  bcval5  10743  hashnncl  10775  fz1f1o  11383  arisum  11506  arisum2  11507  fprodfac  11623  ef0lem  11668  nn0enne  11907  nn0o1gt2  11910  dfgcd2  12015  mulgcd  12017  eucalgf  12055  eucalginv  12056  prmdvdsexpr  12150  rpexp1i  12154  nn0gcdsq  12200  odzdvds  12245  pceq0  12321  fldivp1  12346  pockthg  12355  1arith  12365  mulgnn0p1  12994  mulgnn0subcl  12996  mulgneg  13001  mulgnn0z  13010  mulgnn0dir  13013  mulgnn0ass  13019  dvexp2  14179  lgsdir  14439  lgsabs1  14443  lgseisenlem1  14453  2sqlem7  14471