ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elnn0 Unicode version

Theorem elnn0 9137
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
StepHypRef Expression
1 df-n0 9136 . . 3  |-  NN0  =  ( NN  u.  { 0 } )
21eleq2i 2237 . 2  |-  ( A  e.  NN0  <->  A  e.  ( NN  u.  { 0 } ) )
3 elun 3268 . 2  |-  ( A  e.  ( NN  u.  { 0 } )  <->  ( A  e.  NN  \/  A  e. 
{ 0 } ) )
4 c0ex 7914 . . . 4  |-  0  e.  _V
54elsn2 3617 . . 3  |-  ( A  e.  { 0 }  <-> 
A  =  0 )
65orbi2i 757 . 2  |-  ( ( A  e.  NN  \/  A  e.  { 0 } )  <->  ( A  e.  NN  \/  A  =  0 ) )
72, 3, 63bitri 205 1  |-  ( A  e.  NN0  <->  ( A  e.  NN  \/  A  =  0 ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 104    \/ wo 703    = wceq 1348    e. wcel 2141    u. cun 3119   {csn 3583   0cc0 7774   NNcn 8878   NN0cn0 9135
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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-1cn 7867  ax-icn 7869  ax-addcl 7870  ax-mulcl 7872  ax-i2m1 7879
This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-sn 3589  df-n0 9136
This theorem is referenced by:  0nn0  9150  nn0ge0  9160  nnnn0addcl  9165  nnm1nn0  9176  elnnnn0b  9179  elnn0z  9225  elznn0nn  9226  elznn0  9227  elznn  9228  nn0ind-raph  9329  nn0ledivnn  9724  expp1  10483  expnegap0  10484  expcllem  10487  nn0ltexp2  10644  facp1  10664  faclbnd  10675  faclbnd3  10677  bcn1  10692  bcval5  10697  hashnncl  10730  fz1f1o  11338  arisum  11461  arisum2  11462  fprodfac  11578  ef0lem  11623  nn0enne  11861  nn0o1gt2  11864  dfgcd2  11969  mulgcd  11971  eucalgf  12009  eucalginv  12010  prmdvdsexpr  12104  rpexp1i  12108  nn0gcdsq  12154  odzdvds  12199  pceq0  12275  fldivp1  12300  pockthg  12309  1arith  12319  dvexp2  13470  lgsdir  13730  lgsabs1  13734  2sqlem7  13751
  Copyright terms: Public domain W3C validator