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 2829	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4094	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11129	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4610	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 913	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 297	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 206   ∨ wo 848   = wceq 1542   ∈ wcel 2114   ∪ cun 3888  {csn 4568  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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-mulcl 11091  ax-i2m1 11097

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-sn 4569  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  21422  zringlpirlem3  21454  prmirredlem  21462  prmirred  21464  znf1o  21541  evlslem3  22068  dscmet  24547  dvexp2  25931  tdeglem4  26035  dgrnznn  26222  coefv0  26223  dgreq0  26240  dgrcolem2  26249  dvply1  26260  aaliou2  26317  radcnv0  26394  logfac  26578  logtayl  26637  cxpexp  26645  birthdaylem2  26929  harmonicbnd3  26985  sqf11  27116  ppiltx  27154  sqff1o  27159  lgsdir  27309  lgsabs1  27313  lgseisenlem1  27352  2sqlem7  27401  2sqblem  27408  2sqnn  27416  chebbnd1lem1  27446  nexple  32932  xrsmulgzz  33084  ressmulgnn0d  33120  fldext2rspun  33842  eulerpartlemsv2  34518  eulerpartlemv  34524  eulerpartlemb  34528  eulerpartlemf  34530  eulerpartlemgvv  34536  eulerpartlemgh  34538  fz0n  35929  bccolsum  35937  nn0prpw  36521  aks4d1p1  42529  sticksstones13  42612  negn0nposznnd  42728  dvdsexpnn0  42780  nn0addcom  42921  nn0mulcom  42925  zmulcomlem  42926  fsuppind  43037  fzsplit1nn0  43200  pell1qrgaplem  43319  monotoddzzfi  43388  jm2.22  43441  jm2.23  43442  rmydioph  43460  expdioph  43469  rp-isfinite6  43963  relexpss1d  44150  relexpmulg  44155  iunrelexpmin2  44157  relexp0a  44161  relexpxpmin  44162  relexpaddss  44163  wallispilem3  46513  etransclem24  46704  lighneallem3  48082  lighneallem4  48085  nn0o1gt2ALTV  48182  nn0oALTV  48184  ztprmneprm  48835  blennn0elnn  49065  blen1b  49076  nn0sumshdiglem1  49109