ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elnn0 GIF 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 (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Proof of Theorem elnn0
StepHypRef Expression
1 df-n0 8607 . . 3 0 = (ℕ ∪ {0})
21eleq2i 2151 . 2 (𝐴 ∈ ℕ0𝐴 ∈ (ℕ ∪ {0}))
3 elun 3130 . 2 (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4 c0ex 7426 . . . 4 0 ∈ V
54elsn2 3461 . . 3 (𝐴 ∈ {0} ↔ 𝐴 = 0)
65orbi2i 712 . 2 ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
72, 3, 63bitri 204 1 (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
Colors of variables: wff set class
Syntax hints:  wb 103  wo 662   = wceq 1287  wcel 1436  cun 2986  {csn 3431  0cc0 7294  cn 8357  0cn0 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  9861  expnegap0  9862  expcllem  9865  facp1  10035  faclbnd  10046  faclbnd3  10048  bcn1  10063  ibcval5  10068  hashnncl  10101  fz1f1o  10656  nn0enne  10784  nn0o1gt2  10787  dfgcd2  10885  mulgcd  10887  eucalgf  10919  eucalginv  10920  prmdvdsexpr  11011  rpexp1i  11015  nn0gcdsq  11060
  Copyright terms: Public domain W3C validator