Theorem elnn0 9544

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 9543	. . 3 |- NN0 = ( NN u. { 0 } )
2	1	eleq2i 2305	. 2 |- ( A e. NN0 <-> A e. ( NN u. { 0 } ) )
3		elun 3370	. 2 |- ( A e. ( NN u. { 0 } ) <-> ( A e. NN \/ A e. { 0 } ) )
4		c0ex 8310	. . . 4 |- 0 e. _V
5	4	elsn2 3739	. . 3 |- ( A e. { 0 } <-> A = 0 )
6	5	orbi2i 774	. 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 720   = wceq 1402   e. wcel 2209   u. cun 3218   {csn 3705   0cc0 8169   NNcn 9283   NN0cn0 9542

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-1cn 8262  ax-icn 8264  ax-addcl 8265  ax-mulcl 8267  ax-i2m1 8274

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3711  df-n0 9543

This theorem is referenced by:  0nn0  9557  nn0ge0  9567  nnnn0addcl  9572  nnm1nn0  9583  elnnnn0b  9586  elnn0z  9636  elznn0nn  9637  elznn0  9638  elznn  9639  nn0ind-raph  9742  nn0ledivnn  10147  expp1  10961  expnegap0  10962  expcllem  10965  nn0ltexp2  11125  facp1  11146  faclbnd  11157  faclbnd3  11159  bcn1  11174  bcval5  11179  hashnncl  11212  fz1f1o  12119  arisum  12243  arisum2  12244  fprodfac  12360  ef0lem  12405  nn0enne  12647  nn0o1gt2  12650  dfgcd2  12769  mulgcd  12771  eucalgf  12811  eucalginv  12812  prmdvdsexpr  12906  rpexp1i  12910  nn0gcdsq  12956  odzdvds  13002  pceq0  13079  fldivp1  13105  pockthg  13114  1arith  13124  4sqlem17  13164  4sqlem19  13166  mulgnn0gzsum  13908  mulgnn0p1  13913  mulgnn0subcl  13915  mulgneg  13920  mulgnn0z  13929  mulgnn0dir  13932  mulgnn0ass  13938  submmulg  13946  gsumvalfi  14129  znf1o  14958  dvexp2  15736  dvply1  15789  logfac  15918  lgsdir  16068  lgsabs1  16072  lgseisenlem1  16103  2sqlem7  16154  clwwlknnn  16567