Theorem elnn0 9097

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 9096	. . 3 |- NN0 = ( NN u. { 0 } )
2	1	eleq2i 2224	. 2 |- ( A e. NN0 <-> A e. ( NN u. { 0 } ) )
3		elun 3249	. 2 |- ( A e. ( NN u. { 0 } ) <-> ( A e. NN \/ A e. { 0 } ) )
4		c0ex 7874	. . . 4 |- 0 e. _V
5	4	elsn2 3595	. . 3 |- ( A e. { 0 } <-> A = 0 )
6	5	orbi2i 752	. 2 |- ( ( A e. NN \/ A e. { 0 } ) <-> ( A e. NN \/ A = 0 ) )
7	2, 3, 6	3bitri 205	1 |- ( A e. NN0 <-> ( A e. NN \/ A = 0 ) )

Syntax hints:   <-> wb 104   \/ wo 698   = wceq 1335   e. wcel 2128   u. cun 3100   {csn 3561   0cc0 7734   NNcn 8838   NN0cn0 9095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139  ax-1cn 7827  ax-icn 7829  ax-addcl 7830  ax-mulcl 7832  ax-i2m1 7839

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-v 2714  df-un 3106  df-sn 3567  df-n0 9096

This theorem is referenced by:  0nn0  9110  nn0ge0  9120  nnnn0addcl  9125  nnm1nn0  9136  elnnnn0b  9139  elnn0z  9185  elznn0nn  9186  elznn0  9187  elznn  9188  nn0ind-raph  9286  nn0ledivnn  9680  expp1  10435  expnegap0  10436  expcllem  10439  nn0ltexp2  10595  facp1  10615  faclbnd  10626  faclbnd3  10628  bcn1  10643  bcval5  10648  hashnncl  10681  fz1f1o  11283  arisum  11406  arisum2  11407  fprodfac  11523  ef0lem  11568  nn0enne  11805  nn0o1gt2  11808  dfgcd2  11913  mulgcd  11915  eucalgf  11947  eucalginv  11948  prmdvdsexpr  12040  rpexp1i  12044  nn0gcdsq  12090  odzdvds  12135  dvexp2  13146