Theorem elnn0 12430

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 12429	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2831	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4083	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11129	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4597	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 918	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 298	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 207   ∨ wo 853   = wceq 1547   ∈ wcel 2119   ∪ cun 3881  {csn 4555  0cc0 11029  ℕcn 12165  ℕ₀cn0 12428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-mulcl 11091  ax-i2m1 11097

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-sn 4556  df-n0 12429

This theorem is referenced by:  0nn0  12443  nn0ge0  12453  nnnn0addcl  12458  nnm1nn0  12469  elnnnn0b  12472  nn0sub  12478  elnn0z  12528  elznn0nn  12529  elznn0  12530  elznn  12531  nn0lt10b  12582  nn0ind-raph  12620  nn0ledivnn  13048  expp1  14021  expneg  14022  expcllem  14025  znsqcld  14115  facp1  14231  faclbnd  14243  faclbnd3  14245  faclbnd4lem1  14246  faclbnd4lem3  14248  faclbnd4  14250  bcn1  14266  bcval5  14271  hashv01gt1  14298  hashnncl  14319  seqcoll2  14418  relexpsucl  14984  relexpsucr  14985  relexpcnv  14988  relexprelg  14991  relexpdmg  14995  relexprng  14999  relexpfld  15002  relexpaddg  15006  fz1f1o  15663  arisum  15816  arisum2  15817  pwdif  15824  geomulcvg  15832  fprodfac  15929  ef0lem  16034  nn0enne  16337  nn0o1gt2  16341  bezoutlem3  16501  dfgcd2  16506  mulgcd  16508  nn0rppwr  16521  nn0expgcd  16524  eucalgf  16543  eucalginv  16544  eucalglt  16545  prmdvdsexpr  16678  rpexp1i  16684  nn0gcdsq  16713  odzdvds  16757  pceq0  16833  fldivp1  16859  pockthg  16868  1arith  16889  4sqlem17  16923  4sqlem19  16925  vdwmc2  16941  vdwlem13  16955  0ram  16982  ram0  16984  ramz  16987  ramcl  16991  ressmulgnn0  19044  mulgnn0gsum  19047  mulgnn0p1  19052  mulgnn0subcl  19054  mulgneg  19059  mulgnn0z  19068  mulgnn0dir  19071  mulgnn0ass  19077  submmulg  19085  odcl  19502  mndodcongi  19509  oddvdsnn0  19510  odnncl  19511  oddvds  19513  dfod2  19530  odcl2  19531  gexcl  19546  gexdvds  19550  gexnnod  19554  sylow1lem1  19564  mulgnn0di  19791  torsubg  19820  ablfac1eu  20041  gzrngunitlem  21407  zringlpirlem3  21439  prmirredlem  21447  prmirred  21449  znf1o  21526  evlslem3  22056  dscmet  24555  dvexp2  25939  tdeglem4  26043  dgrnznn  26230  coefv0  26231  dgreq0  26248  dgrcolem2  26257  dvply1  26268  aaliou2  26324  radcnv0  26399  logfac  26583  logtayl  26642  cxpexp  26650  birthdaylem2  26934  harmonicbnd3  26989  sqf11  27120  ppiltx  27158  sqff1o  27163  lgsdir  27313  lgsabs1  27317  lgseisenlem1  27356  2sqlem7  27405  2sqblem  27412  2sqnn  27420  chebbnd1lem1  27450  nexple  32936  xrsmulgzz  33088  ressmulgnn0d  33125  fldext2rspun  33866  eulerpartlemsv2  34542  eulerpartlemv  34548  eulerpartlemb  34552  eulerpartlemf  34554  eulerpartlemgvv  34560  eulerpartlemgh  34562  fz0n  35959  bccolsum  35967  nn0prpw  36551  aks4d1p1  42561  sticksstones13  42644  negn0nposznnd  42759  dvdsexpnn0  42811  nn0addcom  42952  nn0mulcom  42956  zmulcomlem  42957  fsuppind  43040  fzsplit1nn0  43203  pell1qrgaplem  43318  monotoddzzfi  43387  jm2.22  43440  jm2.23  43441  rmydioph  43459  expdioph  43468  rp-isfinite6  43962  relexpss1d  44149  relexpmulg  44154  iunrelexpmin2  44156  relexp0a  44160  relexpxpmin  44161  relexpaddss  44162  wallispilem3  46510  etransclem24  46701  lighneallem3  48085  lighneallem4  48088  nn0o1gt2ALTV  48185  nn0oALTV  48187  ztprmneprm  48838  blennn0elnn  49068  blen1b  49079  nn0sumshdiglem1  49112