Theorem elnn0 12244

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 12243	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2831	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4084	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 10978	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4601	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 910	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 297	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 205   ∨ wo 844   = wceq 1539   ∈ wcel 2107   ∪ cun 3886  {csn 4562  0cc0 10880  ℕcn 11982  ℕ₀cn0 12242

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-mulcl 10942  ax-i2m1 10948

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-un 3893  df-sn 4563  df-n0 12243

This theorem is referenced by:  0nn0  12257  nn0ge0  12267  nnnn0addcl  12272  nnm1nn0  12283  elnnnn0b  12286  nn0sub  12292  elnn0z  12341  elznn0nn  12342  elznn0  12343  elznn  12344  nn0lt10b  12391  nn0ind-raph  12429  nn0ledivnn  12852  expp1  13798  expneg  13799  expcllem  13802  znsqcld  13889  facp1  14001  faclbnd  14013  faclbnd3  14015  faclbnd4lem1  14016  faclbnd4lem3  14018  faclbnd4  14020  bcn1  14036  bcval5  14041  hashv01gt1  14068  hashnncl  14090  seqcoll2  14188  relexpsucl  14751  relexpsucr  14752  relexpcnv  14755  relexprelg  14758  relexpdmg  14762  relexprng  14766  relexpfld  14769  relexpaddg  14773  fz1f1o  15431  arisum  15581  arisum2  15582  pwdif  15589  geomulcvg  15597  fprodfac  15692  ef0lem  15797  nn0enne  16095  nn0o1gt2  16099  bezoutlem3  16258  dfgcd2  16263  mulgcd  16265  eucalgf  16297  eucalginv  16298  eucalglt  16299  prmdvdsexpr  16431  rpexp1i  16437  nn0gcdsq  16465  odzdvds  16505  pceq0  16581  fldivp1  16607  pockthg  16616  1arith  16637  4sqlem17  16671  4sqlem19  16673  vdwmc2  16689  vdwlem13  16703  0ram  16730  ram0  16732  ramz  16735  ramcl  16739  mulgnn0gsum  18719  mulgnn0p1  18724  mulgnn0subcl  18726  mulgneg  18731  mulgnn0z  18739  mulgnn0dir  18742  mulgnn0ass  18748  submmulg  18756  odcl  19153  mndodcongi  19160  oddvdsnn0  19161  odnncl  19162  oddvds  19164  dfod2  19180  odcl2  19181  gexcl  19194  gexdvds  19198  gexnnod  19202  sylow1lem1  19212  mulgnn0di  19436  torsubg  19464  ablfac1eu  19685  gzrngunitlem  20672  zringlpirlem3  20695  prmirredlem  20703  prmirred  20705  znf1o  20768  evlslem3  21299  dscmet  23737  dvexp2  25127  tdeglem4  25233  tdeglem4OLD  25234  dgrnznn  25417  coefv0  25418  dgreq0  25435  dgrcolem2  25444  dvply1  25453  aaliou2  25509  radcnv0  25584  logfac  25765  logtayl  25824  cxpexp  25832  birthdaylem2  26111  harmonicbnd3  26166  sqf11  26297  ppiltx  26335  sqff1o  26340  lgsdir  26489  lgsabs1  26493  lgseisenlem1  26532  2sqlem7  26581  2sqblem  26588  2sqnn  26596  chebbnd1lem1  26626  xrsmulgzz  31296  ressmulgnn0  31302  nexple  31986  eulerpartlemsv2  32334  eulerpartlemv  32340  eulerpartlemb  32344  eulerpartlemf  32346  eulerpartlemgvv  32352  eulerpartlemgh  32354  fz0n  33705  bccolsum  33714  nn0prpw  34521  aks4d1p1  40091  sticksstones13  40122  fsuppind  40286  negn0nposznnd  40317  nn0rppwr  40340  nn0expgcd  40342  dvdsexpnn0  40348  fzsplit1nn0  40583  pell1qrgaplem  40702  monotoddzzfi  40771  jm2.22  40824  jm2.23  40825  rmydioph  40843  expdioph  40852  rp-isfinite6  41132  relexpss1d  41320  relexpmulg  41325  iunrelexpmin2  41327  relexp0a  41331  relexpxpmin  41332  relexpaddss  41333  wallispilem3  43615  etransclem24  43806  lighneallem3  45070  lighneallem4  45073  nn0o1gt2ALTV  45157  nn0oALTV  45159  ztprmneprm  45694  blennn0elnn  45934  blen1b  45945  nn0sumshdiglem1  45978