Theorem elnn0 9463

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 9462	. . 3 |- NN0 = ( NN u. { 0 } )
2	1	eleq2i 2298	. 2 |- ( A e. NN0 <-> A e. ( NN u. { 0 } ) )
3		elun 3350	. 2 |- ( A e. ( NN u. { 0 } ) <-> ( A e. NN \/ A e. { 0 } ) )
4		c0ex 8233	. . . 4 |- 0 e. _V
5	4	elsn2 3707	. . 3 |- ( A e. { 0 } <-> A = 0 )
6	5	orbi2i 770	. 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 716   = wceq 1398   e. wcel 2202   u. cun 3199   {csn 3673   0cc0 8092   NNcn 9202   NN0cn0 9461

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-1cn 8185  ax-icn 8187  ax-addcl 8188  ax-mulcl 8190  ax-i2m1 8197

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-sn 3679  df-n0 9462

This theorem is referenced by:  0nn0  9476  nn0ge0  9486  nnnn0addcl  9491  nnm1nn0  9502  elnnnn0b  9505  elnn0z  9553  elznn0nn  9554  elznn0  9555  elznn  9556  nn0ind-raph  9658  nn0ledivnn  10063  expp1  10871  expnegap0  10872  expcllem  10875  nn0ltexp2  11034  facp1  11055  faclbnd  11066  faclbnd3  11068  bcn1  11083  bcval5  11088  hashnncl  11120  fz1f1o  12015  arisum  12139  arisum2  12140  fprodfac  12256  ef0lem  12301  nn0enne  12543  nn0o1gt2  12546  dfgcd2  12665  mulgcd  12667  eucalgf  12707  eucalginv  12708  prmdvdsexpr  12802  rpexp1i  12806  nn0gcdsq  12852  odzdvds  12898  pceq0  12975  fldivp1  13001  pockthg  13010  1arith  13020  4sqlem17  13060  4sqlem19  13062  mulgnn0gsum  13795  mulgnn0p1  13800  mulgnn0subcl  13802  mulgneg  13807  mulgnn0z  13816  mulgnn0dir  13819  mulgnn0ass  13825  submmulg  13833  znf1o  14747  dvexp2  15523  dvply1  15576  lgsdir  15854  lgsabs1  15858  lgseisenlem1  15889  2sqlem7  15940  clwwlknnn  16353  gfsumval  16809