Theorem elnn0 9404

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 9403	. . 3 |- NN0 = ( NN u. { 0 } )
2	1	eleq2i 2298	. 2 |- ( A e. NN0 <-> A e. ( NN u. { 0 } ) )
3		elun 3348	. 2 |- ( A e. ( NN u. { 0 } ) <-> ( A e. NN \/ A e. { 0 } ) )
4		c0ex 8173	. . . 4 |- 0 e. _V
5	4	elsn2 3703	. . 3 |- ( A e. { 0 } <-> A = 0 )
6	5	orbi2i 769	. 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 715   = wceq 1397   e. wcel 2202   u. cun 3198   {csn 3669   0cc0 8032   NNcn 9143   NN0cn0 9402

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-1cn 8125  ax-icn 8127  ax-addcl 8128  ax-mulcl 8130  ax-i2m1 8137

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-n0 9403

This theorem is referenced by:  0nn0  9417  nn0ge0  9427  nnnn0addcl  9432  nnm1nn0  9443  elnnnn0b  9446  elnn0z  9492  elznn0nn  9493  elznn0  9494  elznn  9495  nn0ind-raph  9597  nn0ledivnn  10002  expp1  10809  expnegap0  10810  expcllem  10813  nn0ltexp2  10972  facp1  10993  faclbnd  11004  faclbnd3  11006  bcn1  11021  bcval5  11026  hashnncl  11058  fz1f1o  11953  arisum  12077  arisum2  12078  fprodfac  12194  ef0lem  12239  nn0enne  12481  nn0o1gt2  12484  dfgcd2  12603  mulgcd  12605  eucalgf  12645  eucalginv  12646  prmdvdsexpr  12740  rpexp1i  12744  nn0gcdsq  12790  odzdvds  12836  pceq0  12913  fldivp1  12939  pockthg  12948  1arith  12958  4sqlem17  12998  4sqlem19  13000  mulgnn0gsum  13733  mulgnn0p1  13738  mulgnn0subcl  13740  mulgneg  13745  mulgnn0z  13754  mulgnn0dir  13757  mulgnn0ass  13763  submmulg  13771  znf1o  14684  dvexp2  15455  dvply1  15508  lgsdir  15783  lgsabs1  15787  lgseisenlem1  15818  2sqlem7  15869  clwwlknnn  16282  gfsumval  16732