Theorem elnn0 12526

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 12525	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2831	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4163	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11253	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4670	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 912	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 297	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 206   ∨ wo 847   = wceq 1537   ∈ wcel 2106   ∪ cun 3961  {csn 4631  0cc0 11153  ℕcn 12264  ℕ₀cn0 12524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-mulcl 11215  ax-i2m1 11221

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-sn 4632  df-n0 12525

This theorem is referenced by:  0nn0  12539  nn0ge0  12549  nnnn0addcl  12554  nnm1nn0  12565  elnnnn0b  12568  nn0sub  12574  elnn0z  12624  elznn0nn  12625  elznn0  12626  elznn  12627  nn0lt10b  12678  nn0ind-raph  12716  nn0ledivnn  13146  expp1  14106  expneg  14107  expcllem  14110  znsqcld  14199  facp1  14314  faclbnd  14326  faclbnd3  14328  faclbnd4lem1  14329  faclbnd4lem3  14331  faclbnd4  14333  bcn1  14349  bcval5  14354  hashv01gt1  14381  hashnncl  14402  seqcoll2  14501  relexpsucl  15067  relexpsucr  15068  relexpcnv  15071  relexprelg  15074  relexpdmg  15078  relexprng  15082  relexpfld  15085  relexpaddg  15089  fz1f1o  15743  arisum  15893  arisum2  15894  pwdif  15901  geomulcvg  15909  fprodfac  16006  ef0lem  16111  nn0enne  16411  nn0o1gt2  16415  bezoutlem3  16575  dfgcd2  16580  mulgcd  16582  nn0rppwr  16595  nn0expgcd  16598  eucalgf  16617  eucalginv  16618  eucalglt  16619  prmdvdsexpr  16751  rpexp1i  16757  nn0gcdsq  16786  odzdvds  16829  pceq0  16905  fldivp1  16931  pockthg  16940  1arith  16961  4sqlem17  16995  4sqlem19  16997  vdwmc2  17013  vdwlem13  17027  0ram  17054  ram0  17056  ramz  17059  ramcl  17063  ressmulgnn0  19108  mulgnn0gsum  19111  mulgnn0p1  19116  mulgnn0subcl  19118  mulgneg  19123  mulgnn0z  19132  mulgnn0dir  19135  mulgnn0ass  19141  submmulg  19149  odcl  19569  mndodcongi  19576  oddvdsnn0  19577  odnncl  19578  oddvds  19580  dfod2  19597  odcl2  19598  gexcl  19613  gexdvds  19617  gexnnod  19621  sylow1lem1  19631  mulgnn0di  19858  torsubg  19887  ablfac1eu  20108  gzrngunitlem  21468  zringlpirlem3  21493  prmirredlem  21501  prmirred  21503  znf1o  21588  evlslem3  22122  dscmet  24601  dvexp2  26007  tdeglem4  26114  dgrnznn  26301  coefv0  26302  dgreq0  26320  dgrcolem2  26329  dvply1  26340  aaliou2  26397  radcnv0  26474  logfac  26658  logtayl  26717  cxpexp  26725  birthdaylem2  27010  harmonicbnd3  27066  sqf11  27197  ppiltx  27235  sqff1o  27240  lgsdir  27391  lgsabs1  27395  lgseisenlem1  27434  2sqlem7  27483  2sqblem  27490  2sqnn  27498  chebbnd1lem1  27528  xrsmulgzz  32994  nexple  33990  eulerpartlemsv2  34340  eulerpartlemv  34346  eulerpartlemb  34350  eulerpartlemf  34352  eulerpartlemgvv  34358  eulerpartlemgh  34360  fz0n  35711  bccolsum  35719  nn0prpw  36306  aks4d1p1  42058  sticksstones13  42141  negn0nposznnd  42296  dvdsexpnn0  42348  nn0addcom  42457  nn0mulcom  42461  zmulcomlem  42462  fsuppind  42577  fzsplit1nn0  42742  pell1qrgaplem  42861  monotoddzzfi  42931  jm2.22  42984  jm2.23  42985  rmydioph  43003  expdioph  43012  rp-isfinite6  43508  relexpss1d  43695  relexpmulg  43700  iunrelexpmin2  43702  relexp0a  43706  relexpxpmin  43707  relexpaddss  43708  wallispilem3  46023  etransclem24  46214  lighneallem3  47532  lighneallem4  47535  nn0o1gt2ALTV  47619  nn0oALTV  47621  ztprmneprm  48192  blennn0elnn  48427  blen1b  48438  nn0sumshdiglem1  48471