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

Theorem elnn0 9154
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 9153 . . 3 0 = (ℕ ∪ {0})
21eleq2i 2244 . 2 (𝐴 ∈ ℕ0𝐴 ∈ (ℕ ∪ {0}))
3 elun 3276 . 2 (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4 c0ex 7929 . . . 4 0 ∈ V
54elsn2 3625 . . 3 (𝐴 ∈ {0} ↔ 𝐴 = 0)
65orbi2i 762 . 2 ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
72, 3, 63bitri 206 1 (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
Colors of variables: wff set class
Syntax hints:  wb 105  wo 708   = wceq 1353  wcel 2148  cun 3127  {csn 3591  0cc0 7789  cn 8895  0cn0 9152
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-1cn 7882  ax-icn 7884  ax-addcl 7885  ax-mulcl 7887  ax-i2m1 7894
This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-sn 3597  df-n0 9153
This theorem is referenced by:  0nn0  9167  nn0ge0  9177  nnnn0addcl  9182  nnm1nn0  9193  elnnnn0b  9196  elnn0z  9242  elznn0nn  9243  elznn0  9244  elznn  9245  nn0ind-raph  9346  nn0ledivnn  9741  expp1  10500  expnegap0  10501  expcllem  10504  nn0ltexp2  10661  facp1  10681  faclbnd  10692  faclbnd3  10694  bcn1  10709  bcval5  10714  hashnncl  10746  fz1f1o  11354  arisum  11477  arisum2  11478  fprodfac  11594  ef0lem  11639  nn0enne  11877  nn0o1gt2  11880  dfgcd2  11985  mulgcd  11987  eucalgf  12025  eucalginv  12026  prmdvdsexpr  12120  rpexp1i  12124  nn0gcdsq  12170  odzdvds  12215  pceq0  12291  fldivp1  12316  pockthg  12325  1arith  12335  mulgnn0p1  12870  mulgnn0subcl  12872  mulgneg  12877  mulgnn0z  12885  mulgnn0dir  12888  mulgnn0ass  12894  dvexp2  13809  lgsdir  14069  lgsabs1  14073  2sqlem7  14090
  Copyright terms: Public domain W3C validator