Theorem elnn0 12444

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 12443	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2820	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4116	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11168	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4629	. . 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 1540   ∈ wcel 2109   ∪ cun 3912  {csn 4589  0cc0 11068  ℕcn 12186  ℕ₀cn0 12442

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-mulcl 11130  ax-i2m1 11136

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-sn 4590  df-n0 12443

This theorem is referenced by:  0nn0  12457  nn0ge0  12467  nnnn0addcl  12472  nnm1nn0  12483  elnnnn0b  12486  nn0sub  12492  elnn0z  12542  elznn0nn  12543  elznn0  12544  elznn  12545  nn0lt10b  12596  nn0ind-raph  12634  nn0ledivnn  13066  expp1  14033  expneg  14034  expcllem  14037  znsqcld  14127  facp1  14243  faclbnd  14255  faclbnd3  14257  faclbnd4lem1  14258  faclbnd4lem3  14260  faclbnd4  14262  bcn1  14278  bcval5  14283  hashv01gt1  14310  hashnncl  14331  seqcoll2  14430  relexpsucl  14997  relexpsucr  14998  relexpcnv  15001  relexprelg  15004  relexpdmg  15008  relexprng  15012  relexpfld  15015  relexpaddg  15019  fz1f1o  15676  arisum  15826  arisum2  15827  pwdif  15834  geomulcvg  15842  fprodfac  15939  ef0lem  16044  nn0enne  16347  nn0o1gt2  16351  bezoutlem3  16511  dfgcd2  16516  mulgcd  16518  nn0rppwr  16531  nn0expgcd  16534  eucalgf  16553  eucalginv  16554  eucalglt  16555  prmdvdsexpr  16687  rpexp1i  16693  nn0gcdsq  16722  odzdvds  16766  pceq0  16842  fldivp1  16868  pockthg  16877  1arith  16898  4sqlem17  16932  4sqlem19  16934  vdwmc2  16950  vdwlem13  16964  0ram  16991  ram0  16993  ramz  16996  ramcl  17000  ressmulgnn0  19009  mulgnn0gsum  19012  mulgnn0p1  19017  mulgnn0subcl  19019  mulgneg  19024  mulgnn0z  19033  mulgnn0dir  19036  mulgnn0ass  19042  submmulg  19050  odcl  19466  mndodcongi  19473  oddvdsnn0  19474  odnncl  19475  oddvds  19477  dfod2  19494  odcl2  19495  gexcl  19510  gexdvds  19514  gexnnod  19518  sylow1lem1  19528  mulgnn0di  19755  torsubg  19784  ablfac1eu  20005  gzrngunitlem  21349  zringlpirlem3  21374  prmirredlem  21382  prmirred  21384  znf1o  21461  evlslem3  21987  dscmet  24460  dvexp2  25858  tdeglem4  25965  dgrnznn  26152  coefv0  26153  dgreq0  26171  dgrcolem2  26180  dvply1  26191  aaliou2  26248  radcnv0  26325  logfac  26510  logtayl  26569  cxpexp  26577  birthdaylem2  26862  harmonicbnd3  26918  sqf11  27049  ppiltx  27087  sqff1o  27092  lgsdir  27243  lgsabs1  27247  lgseisenlem1  27286  2sqlem7  27335  2sqblem  27342  2sqnn  27350  chebbnd1lem1  27380  nexple  32769  xrsmulgzz  32947  ressmulgnn0d  32985  fldext2rspun  33677  eulerpartlemsv2  34349  eulerpartlemv  34355  eulerpartlemb  34359  eulerpartlemf  34361  eulerpartlemgvv  34367  eulerpartlemgh  34369  fz0n  35718  bccolsum  35726  nn0prpw  36311  aks4d1p1  42064  sticksstones13  42147  negn0nposznnd  42270  dvdsexpnn0  42322  nn0addcom  42450  nn0mulcom  42454  zmulcomlem  42455  fsuppind  42578  fzsplit1nn0  42742  pell1qrgaplem  42861  monotoddzzfi  42931  jm2.22  42984  jm2.23  42985  rmydioph  43003  expdioph  43012  rp-isfinite6  43507  relexpss1d  43694  relexpmulg  43699  iunrelexpmin2  43701  relexp0a  43705  relexpxpmin  43706  relexpaddss  43707  wallispilem3  46065  etransclem24  46256  lighneallem3  47608  lighneallem4  47611  nn0o1gt2ALTV  47695  nn0oALTV  47697  ztprmneprm  48335  blennn0elnn  48566  blen1b  48577  nn0sumshdiglem1  48610