Theorem elnn0 12480

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 12479	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2823	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4149	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11214	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4668	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 909	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 296	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 205   ∨ wo 843   = wceq 1539   ∈ wcel 2104   ∪ cun 3947  {csn 4629  0cc0 11114  ℕcn 12218  ℕ₀cn0 12478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-mulcl 11176  ax-i2m1 11182

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-un 3954  df-sn 4630  df-n0 12479

This theorem is referenced by:  0nn0  12493  nn0ge0  12503  nnnn0addcl  12508  nnm1nn0  12519  elnnnn0b  12522  nn0sub  12528  elnn0z  12577  elznn0nn  12578  elznn0  12579  elznn  12580  nn0lt10b  12630  nn0ind-raph  12668  nn0ledivnn  13093  expp1  14040  expneg  14041  expcllem  14044  znsqcld  14133  facp1  14244  faclbnd  14256  faclbnd3  14258  faclbnd4lem1  14259  faclbnd4lem3  14261  faclbnd4  14263  bcn1  14279  bcval5  14284  hashv01gt1  14311  hashnncl  14332  seqcoll2  14432  relexpsucl  14984  relexpsucr  14985  relexpcnv  14988  relexprelg  14991  relexpdmg  14995  relexprng  14999  relexpfld  15002  relexpaddg  15006  fz1f1o  15662  arisum  15812  arisum2  15813  pwdif  15820  geomulcvg  15828  fprodfac  15923  ef0lem  16028  nn0enne  16326  nn0o1gt2  16330  bezoutlem3  16489  dfgcd2  16494  mulgcd  16496  eucalgf  16526  eucalginv  16527  eucalglt  16528  prmdvdsexpr  16660  rpexp1i  16666  nn0gcdsq  16694  odzdvds  16734  pceq0  16810  fldivp1  16836  pockthg  16845  1arith  16866  4sqlem17  16900  4sqlem19  16902  vdwmc2  16918  vdwlem13  16932  0ram  16959  ram0  16961  ramz  16964  ramcl  16968  mulgnn0gsum  18998  mulgnn0p1  19003  mulgnn0subcl  19005  mulgneg  19010  mulgnn0z  19019  mulgnn0dir  19022  mulgnn0ass  19028  submmulg  19036  odcl  19447  mndodcongi  19454  oddvdsnn0  19455  odnncl  19456  oddvds  19458  dfod2  19475  odcl2  19476  gexcl  19491  gexdvds  19495  gexnnod  19499  sylow1lem1  19509  mulgnn0di  19736  torsubg  19765  ablfac1eu  19986  gzrngunitlem  21212  zringlpirlem3  21237  prmirredlem  21245  prmirred  21247  znf1o  21328  evlslem3  21864  dscmet  24303  dvexp2  25705  tdeglem4  25811  tdeglem4OLD  25812  dgrnznn  25995  coefv0  25996  dgreq0  26013  dgrcolem2  26022  dvply1  26031  aaliou2  26087  radcnv0  26162  logfac  26343  logtayl  26402  cxpexp  26410  birthdaylem2  26691  harmonicbnd3  26746  sqf11  26877  ppiltx  26915  sqff1o  26920  lgsdir  27069  lgsabs1  27073  lgseisenlem1  27112  2sqlem7  27161  2sqblem  27168  2sqnn  27176  chebbnd1lem1  27206  xrsmulgzz  32444  ressmulgnn0  32450  nexple  33303  eulerpartlemsv2  33653  eulerpartlemv  33659  eulerpartlemb  33663  eulerpartlemf  33665  eulerpartlemgvv  33671  eulerpartlemgh  33673  fz0n  35002  bccolsum  35011  nn0prpw  35513  aks4d1p1  41249  sticksstones13  41283  fsuppind  41466  negn0nposznnd  41498  nn0rppwr  41528  nn0expgcd  41530  dvdsexpnn0  41536  nn0addcom  41627  nn0mulcom  41631  zmulcomlem  41632  fzsplit1nn0  41796  pell1qrgaplem  41915  monotoddzzfi  41985  jm2.22  42038  jm2.23  42039  rmydioph  42057  expdioph  42066  rp-isfinite6  42573  relexpss1d  42760  relexpmulg  42765  iunrelexpmin2  42767  relexp0a  42771  relexpxpmin  42772  relexpaddss  42773  wallispilem3  45083  etransclem24  45274  lighneallem3  46575  lighneallem4  46578  nn0o1gt2ALTV  46662  nn0oALTV  46664  ztprmneprm  47113  blennn0elnn  47352  blen1b  47363  nn0sumshdiglem1  47396