Theorem elnn0 9500

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 9499	. . 3 |- NN0 = ( NN u. { 0 } )
2	1	eleq2i 2301	. 2 |- ( A e. NN0 <-> A e. ( NN u. { 0 } ) )
3		elun 3362	. 2 |- ( A e. ( NN u. { 0 } ) <-> ( A e. NN \/ A e. { 0 } ) )
4		c0ex 8270	. . . 4 |- 0 e. _V
5	4	elsn2 3725	. . 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 2205   u. cun 3211   {csn 3691   0cc0 8129   NNcn 9239   NN0cn0 9498

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 2216  ax-1cn 8222  ax-icn 8224  ax-addcl 8225  ax-mulcl 8227  ax-i2m1 8234

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3217  df-sn 3697  df-n0 9499

This theorem is referenced by:  0nn0  9513  nn0ge0  9523  nnnn0addcl  9528  nnm1nn0  9539  elnnnn0b  9542  elnn0z  9592  elznn0nn  9593  elznn0  9594  elznn  9595  nn0ind-raph  9698  nn0ledivnn  10103  expp1  10912  expnegap0  10913  expcllem  10916  nn0ltexp2  11075  facp1  11096  faclbnd  11107  faclbnd3  11109  bcn1  11124  bcval5  11129  hashnncl  11162  fz1f1o  12064  arisum  12188  arisum2  12189  fprodfac  12305  ef0lem  12350  nn0enne  12592  nn0o1gt2  12595  dfgcd2  12714  mulgcd  12716  eucalgf  12756  eucalginv  12757  prmdvdsexpr  12851  rpexp1i  12855  nn0gcdsq  12901  odzdvds  12947  pceq0  13024  fldivp1  13050  pockthg  13059  1arith  13069  4sqlem17  13109  4sqlem19  13111  mulgnn0gsum  13862  mulgnn0p1  13867  mulgnn0subcl  13869  mulgneg  13874  mulgnn0z  13883  mulgnn0dir  13886  mulgnn0ass  13892  submmulg  13900  znf1o  14816  dvexp2  15594  dvply1  15647  lgsdir  15925  lgsabs1  15929  lgseisenlem1  15960  2sqlem7  16011  clwwlknnn  16424  gfsumval  16879