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

Theorem elnn0 8608
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 8607 . . 3  |-  NN0  =  ( NN  u.  { 0 } )
21eleq2i 2151 . 2  |-  ( A  e.  NN0  <->  A  e.  ( NN  u.  { 0 } ) )
3 elun 3130 . 2  |-  ( A  e.  ( NN  u.  { 0 } )  <->  ( A  e.  NN  \/  A  e. 
{ 0 } ) )
4 c0ex 7426 . . . 4  |-  0  e.  _V
54elsn2 3461 . . 3  |-  ( A  e.  { 0 }  <-> 
A  =  0 )
65orbi2i 712 . 2  |-  ( ( A  e.  NN  \/  A  e.  { 0 } )  <->  ( A  e.  NN  \/  A  =  0 ) )
72, 3, 63bitri 204 1  |-  ( A  e.  NN0  <->  ( A  e.  NN  \/  A  =  0 ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 103    \/ wo 662    = wceq 1287    e. wcel 1436    u. cun 2986   {csn 3431   0cc0 7294   NNcn 8357   NN0cn0 8606
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-1cn 7382  ax-icn 7384  ax-addcl 7385  ax-mulcl 7387  ax-i2m1 7394
This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-un 2992  df-sn 3437  df-n0 8607
This theorem is referenced by:  0nn0  8621  nn0ge0  8631  nnnn0addcl  8636  nnm1nn0  8647  elnnnn0b  8650  elnn0z  8696  elznn0nn  8697  elznn0  8698  elznn  8699  nn0ind-raph  8796  nn0ledivnn  9170  expp1  9860  expnegap0  9861  expcllem  9864  facp1  10034  faclbnd  10045  faclbnd3  10047  bcn1  10062  ibcval5  10067  hashnncl  10100  fz1f1o  10654  nn0enne  10777  nn0o1gt2  10780  dfgcd2  10878  mulgcd  10880  eucalgf  10912  eucalginv  10913  prmdvdsexpr  11004  rpexp1i  11008  nn0gcdsq  11053
  Copyright terms: Public domain W3C validator