Theorem elnn0 11294

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 11293	. . 3 |- NN0 = ( NN u. { 0 } )
2	1	eleq2i 2693	. 2 |- ( A e. NN0 <-> A e. ( NN u. { 0 } ) )
3		elun 3753	. 2 |- ( A e. ( NN u. { 0 } ) <-> ( A e. NN \/ A e. { 0 } ) )
4		c0ex 10034	. . . 4 |- 0 e. _V
5	4	elsn2 4211	. . 3 |- ( A e. { 0 } <-> A = 0 )
6	5	orbi2i 541	. 2 |- ( ( A e. NN \/ A e. { 0 } ) <-> ( A e. NN \/ A = 0 ) )
7	2, 3, 6	3bitri 286	1 |- ( A e. NN0 <-> ( A e. NN \/ A = 0 ) )

Syntax hints:   <-> wb 196   \/ wo 383   = wceq 1483   e. wcel 1990   u. cun 3572   {csn 4177   0cc0 9936   NNcn 11020   NN0cn0 11292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-mulcl 9998  ax-i2m1 10004

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-sn 4178  df-n0 11293

This theorem is referenced by:  0nn0  11307  nn0ge0  11318  nnnn0addcl  11323  nnm1nn0  11334  elnnnn0b  11337  nn0sub  11343  elnn0z  11390  elznn0nn  11391  elznn0  11392  elznn  11393  nn0lt10b  11439  nn0ind-raph  11477  nn0ledivnn  11941  expp1  12867  expneg  12868  expcllem  12871  facp1  13065  faclbnd  13077  faclbnd3  13079  faclbnd4lem1  13080  faclbnd4lem3  13082  faclbnd4  13084  bcn1  13100  bcval5  13105  hashv01gt1  13133  hashnncl  13157  seqcoll2  13249  relexpsucr  13769  relexpsucl  13773  relexpcnv  13775  relexprelg  13778  relexpdmg  13782  relexprng  13786  relexpfld  13789  relexpaddg  13793  fz1f1o  14441  arisum  14592  arisum2  14593  geomulcvg  14607  fprodfac  14703  ef0lem  14809  nn0enne  15094  nn0o1gt2  15097  bezoutlem3  15258  dfgcd2  15263  mulgcd  15265  eucalgf  15296  eucalginv  15297  eucalglt  15298  prmdvdsexpr  15429  rpexp1i  15433  nn0gcdsq  15460  odzdvds  15500  pceq0  15575  fldivp1  15601  pockthg  15610  1arith  15631  4sqlem17  15665  4sqlem19  15667  vdwmc2  15683  vdwlem13  15697  0ram  15724  ram0  15726  ramz  15729  ramcl  15733  mulgnn0p1  17552  mulgnn0subcl  17554  mulgneg  17560  mulgnn0z  17567  mulgnn0dir  17571  mulgnn0ass  17578  submmulg  17586  odcl  17955  mndodcongi  17962  oddvdsnn0  17963  odnncl  17964  oddvds  17966  dfod2  17981  odcl2  17982  gexcl  17995  gexdvds  17999  gexnnod  18003  sylow1lem1  18013  mulgnn0di  18231  torsubg  18257  ablfac1eu  18472  evlslem3  19514  gzrngunitlem  19811  zringlpirlem3  19834  prmirredlem  19841  prmirred  19843  znf1o  19900  dscmet  22377  dvexp2  23717  tdeglem4  23820  dgrnznn  24003  coefv0  24004  dgreq0  24021  dgrcolem2  24030  dvply1  24039  aaliou2  24095  radcnv0  24170  logfac  24347  logtayl  24406  cxpexp  24414  leibpilem1  24667  birthdaylem2  24679  harmonicbnd3  24734  sqf11  24865  ppiltx  24903  sqff1o  24908  lgsdir  25057  lgsabs1  25061  lgseisenlem1  25100  2sqlem7  25149  2sqblem  25156  chebbnd1lem1  25158  numclwwlkffin0  27215  znsqcld  29512  xrsmulgzz  29678  ressmulgnn0  29684  nexple  30071  eulerpartlemsv2  30420  eulerpartlemv  30426  eulerpartlemb  30430  eulerpartlemf  30432  eulerpartlemgvv  30438  eulerpartlemgh  30440  fz0n  31616  bccolsum  31625  nn0prpw  32318  fzsplit1nn0  37317  pell1qrgaplem  37437  monotoddzzfi  37507  jm2.22  37562  jm2.23  37563  rmydioph  37581  expdioph  37590  rp-isfinite6  37864  relexpss1d  37997  relexpmulg  38002  iunrelexpmin2  38004  relexp0a  38008  relexpxpmin  38009  relexpaddss  38010  wallispilem3  40284  etransclem24  40475  pwdif  41501  lighneallem3  41524  lighneallem4  41527  nn0o1gt2ALTV  41605  nn0oALTV  41607  ztprmneprm  42125  blennn0elnn  42371  blen1b  42382  nn0sumshdiglem1  42415