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

Theorem elnn0 8883
Description: Nonnegative integers expressed in terms of naturals and zero. (Contributed by Raph Levien, 10-Dec-2002.)
Assertion
Ref Expression
elnn0 (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Proof of Theorem elnn0
StepHypRef Expression
1 df-n0 8882 . . 3 0 = (ℕ ∪ {0})
21eleq2i 2181 . 2 (𝐴 ∈ ℕ0𝐴 ∈ (ℕ ∪ {0}))
3 elun 3183 . 2 (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4 c0ex 7684 . . . 4 0 ∈ V
54elsn2 3525 . . 3 (𝐴 ∈ {0} ↔ 𝐴 = 0)
65orbi2i 734 . 2 ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
72, 3, 63bitri 205 1 (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
Colors of variables: wff set class
Syntax hints:  wb 104  wo 680   = wceq 1314  wcel 1463  cun 3035  {csn 3493  0cc0 7547  cn 8630  0cn0 8881
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 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 7638  ax-icn 7640  ax-addcl 7641  ax-mulcl 7643  ax-i2m1 7650
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 2244  df-v 2659  df-un 3041  df-sn 3499  df-n0 8882
This theorem is referenced by:  0nn0  8896  nn0ge0  8906  nnnn0addcl  8911  nnm1nn0  8922  elnnnn0b  8925  elnn0z  8971  elznn0nn  8972  elznn0  8973  elznn  8974  nn0ind-raph  9072  nn0ledivnn  9447  expp1  10193  expnegap0  10194  expcllem  10197  facp1  10369  faclbnd  10380  faclbnd3  10382  bcn1  10397  bcval5  10402  hashnncl  10435  fz1f1o  11036  arisum  11159  arisum2  11160  ef0lem  11217  nn0enne  11447  nn0o1gt2  11450  dfgcd2  11548  mulgcd  11550  eucalgf  11582  eucalginv  11583  prmdvdsexpr  11674  rpexp1i  11678  nn0gcdsq  11723
  Copyright terms: Public domain W3C validator