Theorem elnn0 9253

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 9252	. . 3 |- NN0 = ( NN u. { 0 } )
2	1	eleq2i 2263	. 2 |- ( A e. NN0 <-> A e. ( NN u. { 0 } ) )
3		elun 3305	. 2 |- ( A e. ( NN u. { 0 } ) <-> ( A e. NN \/ A e. { 0 } ) )
4		c0ex 8022	. . . 4 |- 0 e. _V
5	4	elsn2 3657	. . 3 |- ( A e. { 0 } <-> A = 0 )
6	5	orbi2i 763	. 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 709   = wceq 1364   e. wcel 2167   u. cun 3155   {csn 3623   0cc0 7881   NNcn 8992   NN0cn0 9251

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-1cn 7974  ax-icn 7976  ax-addcl 7977  ax-mulcl 7979  ax-i2m1 7986

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3629  df-n0 9252

This theorem is referenced by:  0nn0  9266  nn0ge0  9276  nnnn0addcl  9281  nnm1nn0  9292  elnnnn0b  9295  elnn0z  9341  elznn0nn  9342  elznn0  9343  elznn  9344  nn0ind-raph  9445  nn0ledivnn  9844  expp1  10640  expnegap0  10641  expcllem  10644  nn0ltexp2  10803  facp1  10824  faclbnd  10835  faclbnd3  10837  bcn1  10852  bcval5  10857  hashnncl  10889  fz1f1o  11542  arisum  11665  arisum2  11666  fprodfac  11782  ef0lem  11827  nn0enne  12069  nn0o1gt2  12072  dfgcd2  12191  mulgcd  12193  eucalgf  12233  eucalginv  12234  prmdvdsexpr  12328  rpexp1i  12332  nn0gcdsq  12378  odzdvds  12424  pceq0  12501  fldivp1  12527  pockthg  12536  1arith  12546  4sqlem17  12586  4sqlem19  12588  mulgnn0gsum  13268  mulgnn0p1  13273  mulgnn0subcl  13275  mulgneg  13280  mulgnn0z  13289  mulgnn0dir  13292  mulgnn0ass  13298  submmulg  13306  znf1o  14217  dvexp2  14958  dvply1  15011  lgsdir  15286  lgsabs1  15290  lgseisenlem1  15321  2sqlem7  15372