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

Theorem elnn0 8947
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 8946 . . 3 0 = (ℕ ∪ {0})
21eleq2i 2184 . 2 (𝐴 ∈ ℕ0𝐴 ∈ (ℕ ∪ {0}))
3 elun 3187 . 2 (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4 c0ex 7728 . . . 4 0 ∈ V
54elsn2 3529 . . 3 (𝐴 ∈ {0} ↔ 𝐴 = 0)
65orbi2i 736 . 2 ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
72, 3, 63bitri 205 1 (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
Colors of variables: wff set class
Syntax hints:  wb 104  wo 682   = wceq 1316  wcel 1465  cun 3039  {csn 3497  0cc0 7588  cn 8688  0cn0 8945
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 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-1cn 7681  ax-icn 7683  ax-addcl 7684  ax-mulcl 7686  ax-i2m1 7693
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-v 2662  df-un 3045  df-sn 3503  df-n0 8946
This theorem is referenced by:  0nn0  8960  nn0ge0  8970  nnnn0addcl  8975  nnm1nn0  8986  elnnnn0b  8989  elnn0z  9035  elznn0nn  9036  elznn0  9037  elznn  9038  nn0ind-raph  9136  nn0ledivnn  9522  expp1  10268  expnegap0  10269  expcllem  10272  facp1  10444  faclbnd  10455  faclbnd3  10457  bcn1  10472  bcval5  10477  hashnncl  10510  fz1f1o  11112  arisum  11235  arisum2  11236  ef0lem  11293  nn0enne  11526  nn0o1gt2  11529  dfgcd2  11629  mulgcd  11631  eucalgf  11663  eucalginv  11664  prmdvdsexpr  11755  rpexp1i  11759  nn0gcdsq  11805  dvexp2  12772
  Copyright terms: Public domain W3C validator