Theorem elnn0 9003

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 9002	. . 3 |- NN0 = ( NN u. { 0 } )
2	1	eleq2i 2207	. 2 |- ( A e. NN0 <-> A e. ( NN u. { 0 } ) )
3		elun 3222	. 2 |- ( A e. ( NN u. { 0 } ) <-> ( A e. NN \/ A e. { 0 } ) )
4		c0ex 7784	. . . 4 |- 0 e. _V
5	4	elsn2 3566	. . 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 1332   e. wcel 1481   u. cun 3074   {csn 3532   0cc0 7644   NNcn 8744   NN0cn0 9001

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-1cn 7737  ax-icn 7739  ax-addcl 7740  ax-mulcl 7742  ax-i2m1 7749

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-un 3080  df-sn 3538  df-n0 9002

This theorem is referenced by:  0nn0  9016  nn0ge0  9026  nnnn0addcl  9031  nnm1nn0  9042  elnnnn0b  9045  elnn0z  9091  elznn0nn  9092  elznn0  9093  elznn  9094  nn0ind-raph  9192  nn0ledivnn  9584  expp1  10331  expnegap0  10332  expcllem  10335  facp1  10508  faclbnd  10519  faclbnd3  10521  bcn1  10536  bcval5  10541  hashnncl  10574  fz1f1o  11176  arisum  11299  arisum2  11300  ef0lem  11403  nn0enne  11635  nn0o1gt2  11638  dfgcd2  11738  mulgcd  11740  eucalgf  11772  eucalginv  11773  prmdvdsexpr  11864  rpexp1i  11868  nn0gcdsq  11914  dvexp2  12884