Theorem elnn0 8290

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 8289	. . 3 |- NN0 = ( NN u. { 0 } )
2	1	eleq2i 2145	. 2 |- ( A e. NN0 <-> A e. ( NN u. { 0 } ) )
3		elun 3113	. 2 |- ( A e. ( NN u. { 0 } ) <-> ( A e. NN \/ A e. { 0 } ) )
4		c0ex 7113	. . . 4 |- 0 e. _V
5	4	elsn2 3428	. . 3 |- ( A e. { 0 } <-> A = 0 )
6	5	orbi2i 711	. 2 |- ( ( A e. NN \/ A e. { 0 } ) <-> ( A e. NN \/ A = 0 ) )
7	2, 3, 6	3bitri 204	1 |- ( A e. NN0 <-> ( A e. NN \/ A = 0 ) )

Syntax hints:   <-> wb 103   \/ wo 661   = wceq 1284   e. wcel 1433   u. cun 2971   {csn 3398   0cc0 6981   NNcn 8039   NN0cn0 8288

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-1cn 7069  ax-icn 7071  ax-addcl 7072  ax-mulcl 7074  ax-i2m1 7081

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-v 2603  df-un 2977  df-sn 3404  df-n0 8289

This theorem is referenced by:  0nn0  8303  nn0ge0  8313  nnnn0addcl  8318  nnm1nn0  8329  elnnnn0b  8332  elnn0z  8364  elznn0nn  8365  elznn0  8366  elznn  8367  nn0ind-raph  8464  nn0ledivnn  8838  expp1  9483  expnegap0  9484  expcllem  9487  facp1  9657  faclbnd  9668  faclbnd3  9670  bcn1  9685  ibcval5  9690  nn0enne  10302  nn0o1gt2  10305  dfgcd2  10403  mulgcd  10405  eucalgf  10437  eucalginv  10438  prmdvdsexpr  10529  rpexp1i  10533