Theorem elnn0 9297

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 9296	. . 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 8066	. . . 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 7925   NNcn 9036   NN0cn0 9295

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 8018  ax-icn 8020  ax-addcl 8021  ax-mulcl 8023  ax-i2m1 8030

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 9296

This theorem is referenced by:  0nn0  9310  nn0ge0  9320  nnnn0addcl  9325  nnm1nn0  9336  elnnnn0b  9339  elnn0z  9385  elznn0nn  9386  elznn0  9387  elznn  9388  nn0ind-raph  9490  nn0ledivnn  9889  expp1  10691  expnegap0  10692  expcllem  10695  nn0ltexp2  10854  facp1  10875  faclbnd  10886  faclbnd3  10888  bcn1  10903  bcval5  10908  hashnncl  10940  fz1f1o  11686  arisum  11809  arisum2  11810  fprodfac  11926  ef0lem  11971  nn0enne  12213  nn0o1gt2  12216  dfgcd2  12335  mulgcd  12337  eucalgf  12377  eucalginv  12378  prmdvdsexpr  12472  rpexp1i  12476  nn0gcdsq  12522  odzdvds  12568  pceq0  12645  fldivp1  12671  pockthg  12680  1arith  12690  4sqlem17  12730  4sqlem19  12732  mulgnn0gsum  13464  mulgnn0p1  13469  mulgnn0subcl  13471  mulgneg  13476  mulgnn0z  13485  mulgnn0dir  13488  mulgnn0ass  13494  submmulg  13502  znf1o  14413  dvexp2  15184  dvply1  15237  lgsdir  15512  lgsabs1  15516  lgseisenlem1  15547  2sqlem7  15598