Theorem elnn0 12612

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 12611	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2852	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4152	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11304	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4622	. . 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 1569   ∈ wcel 2144   ∪ cun 4149  {csn 4584  0cc0 11204  ℕcn 12339  ℕ₀cn0 12610

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-1cn 11262  ax-icn 11263  ax-addcl 11264  ax-mulcl 11266  ax-i2m1 11272

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4151  df-sn 4585  df-n0 12611

This theorem is used by:  0nn0  12625  nn0ge0  12635  nnnn0addcl  12640  nnm1nn0  12651  elnnnn0b  12654  nn0sub  12660  elnn0z  12710  elznn0nn  12711  elznn0  12712  elznn  12713  nn0lt10b  12765  nn0ind-raph  12803  nn0ledivnn  13239  expp1  14215  expneg  14216  expcllem  14219  znsqcld  14309  facp1  14426  faclbnd  14438  faclbnd3  14440  faclbnd4lem1  14441  faclbnd4lem3  14443  faclbnd4  14445  bcn1  14461  bcval5  14466  hashv01gt1  14493  hashnncl  14514  seqcoll2  14614  relexpsucl  15190  relexpsucr  15191  relexpcnv  15194  relexprelg  15197  relexpdmg  15201  relexprng  15205  relexpfld  15208  relexpaddg  15212  fz1f1o  15882  arisum  16035  arisum2  16036  pwdif  16043  geomulcvg  16051  fprodfac  16146  ef0lem  16250  nn0enne  16553  nn0o1gt2  16557  bezoutlem3  16720  dfgcd2  16725  mulgcd  16727  nn0rppwr  16741  nn0expgcd  16744  eucalgf  16764  eucalginv  16765  eucalglt  16766  prmdvdsexpr  16899  rpexp1i  16905  nn0gcdsq  16934  odzdvds  16979  pceq0  17055  fldivp1  17081  pockthg  17090  1arith  17111  4sqlem17  17145  4sqlem19  17147  vdwmc2  17163  vdwlem13  17177  0ram  17204  ram0  17206  ramz  17209  ramcl  17213  ressmulgnn0  19293  mulgnn0gsum  19296  mulgnn0p1  19301  mulgnn0subcl  19303  mulgneg  19308  mulgnn0z  19317  mulgnn0dir  19320  mulgnn0ass  19326  submmulg  19334  odcl  19756  mndodcongi  19763  oddvdsnn0  19764  odnncl  19765  oddvds  19767  dfod2  19784  odcl2  19785  gexcl  19800  gexdvds  19804  gexnnod  19808  sylow1lem1  19818  mulgnn0di  20045  torsubg  20074  ablfac1eu  20295  gzrngunitlem  21744  zringlpirlem3  21776  prmirredlem  21784  prmirred  21786  znf1o  21863  evlslem3  22395  dscmet  24897  dvexp2  26280  tdeglem4  26384  dgrnznn  26572  coefv0  26573  dgreq0  26590  dgrcolem2  26599  dvply1  26611  aaliou2  26673  radcnv0  26749  logfac  26935  logtayl  26994  cxpexp  27002  birthdaylem2  27286  harmonicbnd3  27341  sqf11  27472  ppiltx  27510  sqff1o  27515  lgsdir  27665  lgsabs1  27669  lgseisenlem1  27708  2sqlem7  27757  2sqblem  27764  2sqnn  27772  chebbnd1lem1  27802  nexple  33471  xrsmulgzz  33617  ressmulgnn0d  33652  fldext2rspun  34361  eulerpartlemsv2  35037  eulerpartlemv  35043  eulerpartlemb  35047  eulerpartlemf  35049  eulerpartlemgvv  35055  eulerpartlemgh  35057  fz0n  36589  bccolsum  36597  nn0prpw  37204  aks4d1p1  43220  sticksstones13  43303  negn0nposznnd  43433  dvdsexpnn0  43480  nn0addcom  43620  nn0mulcom  43624  zmulcomlem  43625  fsuppind  43712  fzsplit1nn0  43859  pell1qrgaplem  43974  monotoddzzfi  44043  jm2.22  44096  jm2.23  44097  rmydioph  44115  expdioph  44124  rp-isfinite6  44613  relexpss1d  44799  relexpmulg  44804  iunrelexpmin2  44806  relexp0a  44810  relexpxpmin  44811  relexpaddss  44812  wallispilem3  47171  etransclem24  47362  lighneallem3  48786  lighneallem4  48789  nn0o1gt2ALTV  48886  nn0oALTV  48888  ztprmneprm  49553  blennn0elnn  49783  blen1b  49794  nn0sumshdiglem1  49827