Theorem elnn0 12434

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 12433	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2833	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4085	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11134	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4599	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 919	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 299	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 208   ∨ wo 854   = wceq 1548   ∈ wcel 2121   ∪ cun 3882  {csn 4557  0cc0 11034  ℕcn 12169  ℕ₀cn0 12432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-1cn 11092  ax-icn 11093  ax-addcl 11094  ax-mulcl 11096  ax-i2m1 11102

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-un 3889  df-sn 4558  df-n0 12433

This theorem is referenced by:  0nn0  12447  nn0ge0  12457  nnnn0addcl  12462  nnm1nn0  12473  elnnnn0b  12476  nn0sub  12482  elnn0z  12532  elznn0nn  12533  elznn0  12534  elznn  12535  nn0lt10b  12586  nn0ind-raph  12624  nn0ledivnn  13052  expp1  14025  expneg  14026  expcllem  14029  znsqcld  14119  facp1  14235  faclbnd  14247  faclbnd3  14249  faclbnd4lem1  14250  faclbnd4lem3  14252  faclbnd4  14254  bcn1  14270  bcval5  14275  hashv01gt1  14302  hashnncl  14323  seqcoll2  14422  relexpsucl  14988  relexpsucr  14989  relexpcnv  14992  relexprelg  14995  relexpdmg  14999  relexprng  15003  relexpfld  15006  relexpaddg  15010  fz1f1o  15667  arisum  15820  arisum2  15821  pwdif  15828  geomulcvg  15836  fprodfac  15933  ef0lem  16038  nn0enne  16341  nn0o1gt2  16345  bezoutlem3  16505  dfgcd2  16510  mulgcd  16512  nn0rppwr  16525  nn0expgcd  16528  eucalgf  16547  eucalginv  16548  eucalglt  16549  prmdvdsexpr  16682  rpexp1i  16688  nn0gcdsq  16717  odzdvds  16761  pceq0  16837  fldivp1  16863  pockthg  16872  1arith  16893  4sqlem17  16927  4sqlem19  16929  vdwmc2  16945  vdwlem13  16959  0ram  16986  ram0  16988  ramz  16991  ramcl  16995  ressmulgnn0  19048  mulgnn0gsum  19051  mulgnn0p1  19056  mulgnn0subcl  19058  mulgneg  19063  mulgnn0z  19072  mulgnn0dir  19075  mulgnn0ass  19081  submmulg  19089  odcl  19505  mndodcongi  19512  oddvdsnn0  19513  odnncl  19514  oddvds  19516  dfod2  19533  odcl2  19534  gexcl  19549  gexdvds  19553  gexnnod  19557  sylow1lem1  19567  mulgnn0di  19794  torsubg  19823  ablfac1eu  20044  gzrngunitlem  21410  zringlpirlem3  21442  prmirredlem  21450  prmirred  21452  znf1o  21529  evlslem3  22059  dscmet  24558  dvexp2  25942  tdeglem4  26046  dgrnznn  26233  coefv0  26234  dgreq0  26251  dgrcolem2  26260  dvply1  26271  aaliou2  26327  radcnv0  26402  logfac  26586  logtayl  26645  cxpexp  26653  birthdaylem2  26937  harmonicbnd3  26992  sqf11  27123  ppiltx  27161  sqff1o  27166  lgsdir  27316  lgsabs1  27320  lgseisenlem1  27359  2sqlem7  27408  2sqblem  27415  2sqnn  27423  chebbnd1lem1  27453  nexple  32938  xrsmulgzz  33090  ressmulgnn0d  33127  fldext2rspun  33876  eulerpartlemsv2  34552  eulerpartlemv  34558  eulerpartlemb  34562  eulerpartlemf  34564  eulerpartlemgvv  34570  eulerpartlemgh  34572  fz0n  35972  bccolsum  35980  nn0prpw  36564  aks4d1p1  42574  sticksstones13  42657  negn0nposznnd  42772  dvdsexpnn0  42824  nn0addcom  42965  nn0mulcom  42969  zmulcomlem  42970  fsuppind  43053  fzsplit1nn0  43216  pell1qrgaplem  43331  monotoddzzfi  43400  jm2.22  43453  jm2.23  43454  rmydioph  43472  expdioph  43481  rp-isfinite6  43975  relexpss1d  44162  relexpmulg  44167  iunrelexpmin2  44169  relexp0a  44173  relexpxpmin  44174  relexpaddss  44175  wallispilem3  46522  etransclem24  46713  lighneallem3  48097  lighneallem4  48100  nn0o1gt2ALTV  48197  nn0oALTV  48199  ztprmneprm  48850  blennn0elnn  49080  blen1b  49091  nn0sumshdiglem1  49124