Theorem elnn0 12646

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 12645	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2856	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4155	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11337	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4626	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 926	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 300	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861   = wceq 1570   ∈ wcel 2147   ∪ cun 4152  {csn 4588  0cc0 11237  ℕcn 12373  ℕ₀cn0 12644

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11295  ax-icn 11296  ax-addcl 11297  ax-mulcl 11299  ax-i2m1 11305

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-sn 4589  df-n0 12645

This theorem is used by:  0nn0  12659  nn0ge0  12669  nnnn0addcl  12674  nnm1nn0  12685  elnnnn0b  12688  nn0sub  12694  elnn0z  12744  elznn0nn  12745  elznn0  12746  elznn  12747  nn0lt10b  12799  nn0ind-raph  12837  nn0ledivnn  13273  expp1  14249  expneg  14250  expcllem  14253  znsqcld  14343  facp1  14461  faclbnd  14473  faclbnd3  14475  faclbnd4lem1  14476  faclbnd4lem3  14478  faclbnd4  14480  bcn1  14496  bcval5  14501  hashv01gt1  14528  hashnncl  14549  seqcoll2  14649  relexpsucl  15225  relexpsucr  15226  relexpcnv  15229  relexprelg  15232  relexpdmg  15236  relexprng  15240  relexpfld  15243  relexpaddg  15247  fz1f1o  15917  arisum  16070  arisum2  16071  pwdif  16078  geomulcvg  16086  fprodfac  16181  ef0lem  16285  nn0enne  16588  nn0o1gt2  16592  bezoutlem3  16755  dfgcd2  16760  mulgcd  16762  nn0rppwr  16776  nn0expgcd  16779  eucalgf  16799  eucalginv  16800  eucalglt  16801  prmdvdsexpr  16934  rpexp1i  16940  nn0gcdsq  16969  odzdvds  17014  pceq0  17090  fldivp1  17116  pockthg  17125  1arith  17146  4sqlem17  17180  4sqlem19  17182  vdwmc2  17198  vdwlem13  17212  0ram  17239  ram0  17241  ramz  17244  ramcl  17248  ressmulgnn0  19328  mulgnn0gsum  19331  mulgnn0p1  19336  mulgnn0subcl  19338  mulgneg  19343  mulgnn0z  19352  mulgnn0dir  19355  mulgnn0ass  19361  submmulg  19369  odcl  19792  mndodcongi  19799  oddvdsnn0  19800  odnncl  19801  oddvds  19803  dfod2  19820  odcl2  19821  gexcl  19836  gexdvds  19840  gexnnod  19844  sylow1lem1  19854  mulgnn0di  20081  torsubg  20110  ablfac1eu  20331  gzrngunitlem  21782  zringlpirlem3  21814  prmirredlem  21822  prmirred  21824  znf1o  21901  evlslem3  22433  dscmet  24935  dvexp2  26318  tdeglem4  26422  dgrnznn  26610  coefv0  26611  dgreq0  26628  dgrcolem2  26637  dvply1  26649  aaliou2  26713  radcnv0  26789  logfac  26975  logtayl  27034  cxpexp  27042  birthdaylem2  27326  harmonicbnd3  27381  sqf11  27512  ppiltx  27550  sqff1o  27555  lgsdir  27705  lgsabs1  27709  lgseisenlem1  27748  2sqlem7  27797  2sqblem  27804  2sqnn  27812  chebbnd1lem1  27842  nexple  33510  xrsmulgzz  33659  ressmulgnn0d  33694  fldext2rspun  34418  eulerpartlemsv2  35094  eulerpartlemv  35100  eulerpartlemb  35104  eulerpartlemf  35106  eulerpartlemgvv  35112  eulerpartlemgh  35114  fz0n  36704  bccolsum  36712  nn0prpw  37319  aks4d1p1  43385  sticksstones13  43468  negn0nposznnd  43599  dvdsexpnn0  43646  nn0addcom  43786  nn0mulcom  43790  zmulcomlem  43791  fsuppind  43878  fzsplit1nn0  44025  pell1qrgaplem  44140  monotoddzzfi  44209  jm2.22  44262  jm2.23  44263  rmydioph  44281  expdioph  44290  rp-isfinite6  44774  relexpss1d  44960  relexpmulg  44965  iunrelexpmin2  44967  relexp0a  44971  relexpxpmin  44972  relexpaddss  44973  wallispilem3  47344  etransclem24  47535  lighneallem3  48959  lighneallem4  48962  nn0o1gt2ALTV  49059  nn0oALTV  49061  ztprmneprm  49784  blennn0elnn  50014  blen1b  50025  nn0sumshdiglem1  50058