Theorem elnn0 12555

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

Step	Hyp	Ref	Expression
1		df-n0 12554	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2836	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4176	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11284	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4687	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 911	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 297	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 206   ∨ wo 846   = wceq 1537   ∈ wcel 2108   ∪ cun 3974  {csn 4648  0cc0 11184  ℕcn 12293  ℕ₀cn0 12553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-mulcl 11246  ax-i2m1 11252

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-sn 4649  df-n0 12554

This theorem is referenced by:  0nn0  12568  nn0ge0  12578  nnnn0addcl  12583  nnm1nn0  12594  elnnnn0b  12597  nn0sub  12603  elnn0z  12652  elznn0nn  12653  elznn0  12654  elznn  12655  nn0lt10b  12705  nn0ind-raph  12743  nn0ledivnn  13170  expp1  14119  expneg  14120  expcllem  14123  znsqcld  14212  facp1  14327  faclbnd  14339  faclbnd3  14341  faclbnd4lem1  14342  faclbnd4lem3  14344  faclbnd4  14346  bcn1  14362  bcval5  14367  hashv01gt1  14394  hashnncl  14415  seqcoll2  14514  relexpsucl  15080  relexpsucr  15081  relexpcnv  15084  relexprelg  15087  relexpdmg  15091  relexprng  15095  relexpfld  15098  relexpaddg  15102  fz1f1o  15758  arisum  15908  arisum2  15909  pwdif  15916  geomulcvg  15924  fprodfac  16021  ef0lem  16126  nn0enne  16425  nn0o1gt2  16429  bezoutlem3  16588  dfgcd2  16593  mulgcd  16595  nn0rppwr  16608  nn0expgcd  16611  eucalgf  16630  eucalginv  16631  eucalglt  16632  prmdvdsexpr  16764  rpexp1i  16770  nn0gcdsq  16799  odzdvds  16842  pceq0  16918  fldivp1  16944  pockthg  16953  1arith  16974  4sqlem17  17008  4sqlem19  17010  vdwmc2  17026  vdwlem13  17040  0ram  17067  ram0  17069  ramz  17072  ramcl  17076  ressmulgnn0  19117  mulgnn0gsum  19120  mulgnn0p1  19125  mulgnn0subcl  19127  mulgneg  19132  mulgnn0z  19141  mulgnn0dir  19144  mulgnn0ass  19150  submmulg  19158  odcl  19578  mndodcongi  19585  oddvdsnn0  19586  odnncl  19587  oddvds  19589  dfod2  19606  odcl2  19607  gexcl  19622  gexdvds  19626  gexnnod  19630  sylow1lem1  19640  mulgnn0di  19867  torsubg  19896  ablfac1eu  20117  gzrngunitlem  21473  zringlpirlem3  21498  prmirredlem  21506  prmirred  21508  znf1o  21593  evlslem3  22127  dscmet  24606  dvexp2  26012  tdeglem4  26119  dgrnznn  26306  coefv0  26307  dgreq0  26325  dgrcolem2  26334  dvply1  26343  aaliou2  26400  radcnv0  26477  logfac  26661  logtayl  26720  cxpexp  26728  birthdaylem2  27013  harmonicbnd3  27069  sqf11  27200  ppiltx  27238  sqff1o  27243  lgsdir  27394  lgsabs1  27398  lgseisenlem1  27437  2sqlem7  27486  2sqblem  27493  2sqnn  27501  chebbnd1lem1  27531  xrsmulgzz  32992  nexple  33973  eulerpartlemsv2  34323  eulerpartlemv  34329  eulerpartlemb  34333  eulerpartlemf  34335  eulerpartlemgvv  34341  eulerpartlemgh  34343  fz0n  35693  bccolsum  35701  nn0prpw  36289  aks4d1p1  42033  sticksstones13  42116  negn0nposznnd  42271  dvdsexpnn0  42321  nn0addcom  42426  nn0mulcom  42430  zmulcomlem  42431  fsuppind  42545  fzsplit1nn0  42710  pell1qrgaplem  42829  monotoddzzfi  42899  jm2.22  42952  jm2.23  42953  rmydioph  42971  expdioph  42980  rp-isfinite6  43480  relexpss1d  43667  relexpmulg  43672  iunrelexpmin2  43674  relexp0a  43678  relexpxpmin  43679  relexpaddss  43680  wallispilem3  45988  etransclem24  46179  lighneallem3  47481  lighneallem4  47484  nn0o1gt2ALTV  47568  nn0oALTV  47570  ztprmneprm  48072  blennn0elnn  48311  blen1b  48322  nn0sumshdiglem1  48355