Theorem elnn0 12530

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 12529	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2852	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4100	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11224	. . . 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 2145   ∪ cun 3897  {csn 4584  0cc0 11124  ℕcn 12257  ℕ₀cn0 12528

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-mulcl 11186  ax-i2m1 11192

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-sn 4585  df-n0 12529

This theorem is used by:  0nn0  12543  nn0ge0  12553  nnnn0addcl  12558  nnm1nn0  12569  elnnnn0b  12572  nn0sub  12578  elnn0z  12628  elznn0nn  12629  elznn0  12630  elznn  12631  nn0lt10b  12683  nn0ind-raph  12721  nn0ledivnn  13157  expp1  14132  expneg  14133  expcllem  14136  znsqcld  14226  facp1  14342  faclbnd  14354  faclbnd3  14356  faclbnd4lem1  14357  faclbnd4lem3  14359  faclbnd4  14361  bcn1  14377  bcval5  14382  hashv01gt1  14409  hashnncl  14430  seqcoll2  14530  relexpsucl  15104  relexpsucr  15105  relexpcnv  15108  relexprelg  15111  relexpdmg  15115  relexprng  15119  relexpfld  15122  relexpaddg  15126  fz1f1o  15796  arisum  15949  arisum2  15950  pwdif  15957  geomulcvg  15965  fprodfac  16060  ef0lem  16164  nn0enne  16467  nn0o1gt2  16471  bezoutlem3  16631  dfgcd2  16636  mulgcd  16638  nn0rppwr  16651  nn0expgcd  16654  eucalgf  16673  eucalginv  16674  eucalglt  16675  prmdvdsexpr  16808  rpexp1i  16814  nn0gcdsq  16843  odzdvds  16887  pceq0  16963  fldivp1  16989  pockthg  16998  1arith  17019  4sqlem17  17053  4sqlem19  17055  vdwmc2  17071  vdwlem13  17085  0ram  17112  ram0  17114  ramz  17117  ramcl  17121  ressmulgnn0  19200  mulgnn0gsum  19203  mulgnn0p1  19208  mulgnn0subcl  19210  mulgneg  19215  mulgnn0z  19224  mulgnn0dir  19227  mulgnn0ass  19233  submmulg  19241  odcl  19663  mndodcongi  19670  oddvdsnn0  19671  odnncl  19672  oddvds  19674  dfod2  19691  odcl2  19692  gexcl  19707  gexdvds  19711  gexnnod  19715  sylow1lem1  19725  mulgnn0di  19952  torsubg  19981  ablfac1eu  20202  gzrngunitlem  21645  zringlpirlem3  21677  prmirredlem  21685  prmirred  21687  znf1o  21764  evlslem3  22296  dscmet  24798  dvexp2  26181  tdeglem4  26285  dgrnznn  26473  coefv0  26474  dgreq0  26491  dgrcolem2  26500  dvply1  26514  aaliou2  26576  radcnv0  26652  logfac  26838  logtayl  26897  cxpexp  26905  birthdaylem2  27189  harmonicbnd3  27244  sqf11  27375  ppiltx  27413  sqff1o  27418  lgsdir  27568  lgsabs1  27572  lgseisenlem1  27611  2sqlem7  27660  2sqblem  27667  2sqnn  27675  chebbnd1lem1  27705  nexple  33303  xrsmulgzz  33449  ressmulgnn0d  33484  fldext2rspun  34192  eulerpartlemsv2  34869  eulerpartlemv  34875  eulerpartlemb  34879  eulerpartlemf  34881  eulerpartlemgvv  34887  eulerpartlemgh  34889  fz0n  36310  bccolsum  36318  nn0prpw  36942  aks4d1p1  42942  sticksstones13  43025  negn0nposznnd  43157  dvdsexpnn0  43209  nn0addcom  43350  nn0mulcom  43354  zmulcomlem  43355  fsuppind  43436  fzsplit1nn0  43599  pell1qrgaplem  43714  monotoddzzfi  43783  jm2.22  43836  jm2.23  43837  rmydioph  43855  expdioph  43864  rp-isfinite6  44358  relexpss1d  44545  relexpmulg  44550  iunrelexpmin2  44552  relexp0a  44556  relexpxpmin  44557  relexpaddss  44558  wallispilem3  46895  etransclem24  47086  lighneallem3  48510  lighneallem4  48513  nn0o1gt2ALTV  48610  nn0oALTV  48612  ztprmneprm  49277  blennn0elnn  49507  blen1b  49518  nn0sumshdiglem1  49551