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

Theorem elnn0 8933
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 8932 . . 3  |-  NN0  =  ( NN  u.  { 0 } )
21eleq2i 2182 . 2  |-  ( A  e.  NN0  <->  A  e.  ( NN  u.  { 0 } ) )
3 elun 3185 . 2  |-  ( A  e.  ( NN  u.  { 0 } )  <->  ( A  e.  NN  \/  A  e. 
{ 0 } ) )
4 c0ex 7724 . . . 4  |-  0  e.  _V
54elsn2 3527 . . 3  |-  ( A  e.  { 0 }  <-> 
A  =  0 )
65orbi2i 734 . 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 680    = wceq 1314    e. wcel 1463    u. cun 3037   {csn 3495   0cc0 7584   NNcn 8680   NN0cn0 8931
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 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-1cn 7677  ax-icn 7679  ax-addcl 7680  ax-mulcl 7682  ax-i2m1 7689
This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-v 2660  df-un 3043  df-sn 3501  df-n0 8932
This theorem is referenced by:  0nn0  8946  nn0ge0  8956  nnnn0addcl  8961  nnm1nn0  8972  elnnnn0b  8975  elnn0z  9021  elznn0nn  9022  elznn0  9023  elznn  9024  nn0ind-raph  9122  nn0ledivnn  9505  expp1  10251  expnegap0  10252  expcllem  10255  facp1  10427  faclbnd  10438  faclbnd3  10440  bcn1  10455  bcval5  10460  hashnncl  10493  fz1f1o  11095  arisum  11218  arisum2  11219  ef0lem  11276  nn0enne  11506  nn0o1gt2  11509  dfgcd2  11609  mulgcd  11611  eucalgf  11643  eucalginv  11644  prmdvdsexpr  11735  rpexp1i  11739  nn0gcdsq  11784  dvexp2  12751
  Copyright terms: Public domain W3C validator