Theorem elnn0 9181

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 9180	. . 3 |- NN0 = ( NN u. { 0 } )
2	1	eleq2i 2244	. 2 |- ( A e. NN0 <-> A e. ( NN u. { 0 } ) )
3		elun 3278	. 2 |- ( A e. ( NN u. { 0 } ) <-> ( A e. NN \/ A e. { 0 } ) )
4		c0ex 7954	. . . 4 |- 0 e. _V
5	4	elsn2 3628	. . 3 |- ( A e. { 0 } <-> A = 0 )
6	5	orbi2i 762	. 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 708   = wceq 1353   e. wcel 2148   u. cun 3129   {csn 3594   0cc0 7814   NNcn 8922   NN0cn0 9179

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-1cn 7907  ax-icn 7909  ax-addcl 7910  ax-mulcl 7912  ax-i2m1 7919

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2741  df-un 3135  df-sn 3600  df-n0 9180

This theorem is referenced by:  0nn0  9194  nn0ge0  9204  nnnn0addcl  9209  nnm1nn0  9220  elnnnn0b  9223  elnn0z  9269  elznn0nn  9270  elznn0  9271  elznn  9272  nn0ind-raph  9373  nn0ledivnn  9770  expp1  10530  expnegap0  10531  expcllem  10534  nn0ltexp2  10692  facp1  10713  faclbnd  10724  faclbnd3  10726  bcn1  10741  bcval5  10746  hashnncl  10778  fz1f1o  11386  arisum  11509  arisum2  11510  fprodfac  11626  ef0lem  11671  nn0enne  11910  nn0o1gt2  11913  dfgcd2  12018  mulgcd  12020  eucalgf  12058  eucalginv  12059  prmdvdsexpr  12153  rpexp1i  12157  nn0gcdsq  12203  odzdvds  12248  pceq0  12324  fldivp1  12349  pockthg  12358  1arith  12368  mulgnn0p1  13008  mulgnn0subcl  13010  mulgneg  13015  mulgnn0z  13024  mulgnn0dir  13027  mulgnn0ass  13033  dvexp2  14364  lgsdir  14624  lgsabs1  14628  lgseisenlem1  14638  2sqlem7  14656