Theorem elnn0 9371

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 9370	. . 3 |- NN0 = ( NN u. { 0 } )
2	1	eleq2i 2296	. 2 |- ( A e. NN0 <-> A e. ( NN u. { 0 } ) )
3		elun 3345	. 2 |- ( A e. ( NN u. { 0 } ) <-> ( A e. NN \/ A e. { 0 } ) )
4		c0ex 8140	. . . 4 |- 0 e. _V
5	4	elsn2 3700	. . 3 |- ( A e. { 0 } <-> A = 0 )
6	5	orbi2i 767	. 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 713   = wceq 1395   e. wcel 2200   u. cun 3195   {csn 3666   0cc0 7999   NNcn 9110   NN0cn0 9369

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1cn 8092  ax-icn 8094  ax-addcl 8095  ax-mulcl 8097  ax-i2m1 8104

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-n0 9370

This theorem is referenced by:  0nn0  9384  nn0ge0  9394  nnnn0addcl  9399  nnm1nn0  9410  elnnnn0b  9413  elnn0z  9459  elznn0nn  9460  elznn0  9461  elznn  9462  nn0ind-raph  9564  nn0ledivnn  9963  expp1  10768  expnegap0  10769  expcllem  10772  nn0ltexp2  10931  facp1  10952  faclbnd  10963  faclbnd3  10965  bcn1  10980  bcval5  10985  hashnncl  11017  fz1f1o  11886  arisum  12009  arisum2  12010  fprodfac  12126  ef0lem  12171  nn0enne  12413  nn0o1gt2  12416  dfgcd2  12535  mulgcd  12537  eucalgf  12577  eucalginv  12578  prmdvdsexpr  12672  rpexp1i  12676  nn0gcdsq  12722  odzdvds  12768  pceq0  12845  fldivp1  12871  pockthg  12880  1arith  12890  4sqlem17  12930  4sqlem19  12932  mulgnn0gsum  13665  mulgnn0p1  13670  mulgnn0subcl  13672  mulgneg  13677  mulgnn0z  13686  mulgnn0dir  13689  mulgnn0ass  13695  submmulg  13703  znf1o  14615  dvexp2  15386  dvply1  15439  lgsdir  15714  lgsabs1  15718  lgseisenlem1  15749  2sqlem7  15800