Theorem elnn0 12470

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 12469	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2825	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4147	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11204	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4666	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 911	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 296	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 205   ∨ wo 845   = wceq 1541   ∈ wcel 2106   ∪ cun 3945  {csn 4627  0cc0 11106  ℕcn 12208  ℕ₀cn0 12468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-mulcl 11168  ax-i2m1 11174

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3952  df-sn 4628  df-n0 12469

This theorem is referenced by:  0nn0  12483  nn0ge0  12493  nnnn0addcl  12498  nnm1nn0  12509  elnnnn0b  12512  nn0sub  12518  elnn0z  12567  elznn0nn  12568  elznn0  12569  elznn  12570  nn0lt10b  12620  nn0ind-raph  12658  nn0ledivnn  13083  expp1  14030  expneg  14031  expcllem  14034  znsqcld  14123  facp1  14234  faclbnd  14246  faclbnd3  14248  faclbnd4lem1  14249  faclbnd4lem3  14251  faclbnd4  14253  bcn1  14269  bcval5  14274  hashv01gt1  14301  hashnncl  14322  seqcoll2  14422  relexpsucl  14974  relexpsucr  14975  relexpcnv  14978  relexprelg  14981  relexpdmg  14985  relexprng  14989  relexpfld  14992  relexpaddg  14996  fz1f1o  15652  arisum  15802  arisum2  15803  pwdif  15810  geomulcvg  15818  fprodfac  15913  ef0lem  16018  nn0enne  16316  nn0o1gt2  16320  bezoutlem3  16479  dfgcd2  16484  mulgcd  16486  eucalgf  16516  eucalginv  16517  eucalglt  16518  prmdvdsexpr  16650  rpexp1i  16656  nn0gcdsq  16684  odzdvds  16724  pceq0  16800  fldivp1  16826  pockthg  16835  1arith  16856  4sqlem17  16890  4sqlem19  16892  vdwmc2  16908  vdwlem13  16922  0ram  16949  ram0  16951  ramz  16954  ramcl  16958  mulgnn0gsum  18954  mulgnn0p1  18959  mulgnn0subcl  18961  mulgneg  18966  mulgnn0z  18975  mulgnn0dir  18978  mulgnn0ass  18984  submmulg  18992  odcl  19398  mndodcongi  19405  oddvdsnn0  19406  odnncl  19407  oddvds  19409  dfod2  19426  odcl2  19427  gexcl  19442  gexdvds  19446  gexnnod  19450  sylow1lem1  19460  mulgnn0di  19687  torsubg  19716  ablfac1eu  19937  gzrngunitlem  21002  zringlpirlem3  21025  prmirredlem  21033  prmirred  21035  znf1o  21098  evlslem3  21634  dscmet  24072  dvexp2  25462  tdeglem4  25568  tdeglem4OLD  25569  dgrnznn  25752  coefv0  25753  dgreq0  25770  dgrcolem2  25779  dvply1  25788  aaliou2  25844  radcnv0  25919  logfac  26100  logtayl  26159  cxpexp  26167  birthdaylem2  26446  harmonicbnd3  26501  sqf11  26632  ppiltx  26670  sqff1o  26675  lgsdir  26824  lgsabs1  26828  lgseisenlem1  26867  2sqlem7  26916  2sqblem  26923  2sqnn  26931  chebbnd1lem1  26961  xrsmulgzz  32166  ressmulgnn0  32172  nexple  32995  eulerpartlemsv2  33345  eulerpartlemv  33351  eulerpartlemb  33355  eulerpartlemf  33357  eulerpartlemgvv  33363  eulerpartlemgh  33365  fz0n  34688  bccolsum  34697  nn0prpw  35196  aks4d1p1  40929  sticksstones13  40963  fsuppind  41159  negn0nposznnd  41191  nn0rppwr  41219  nn0expgcd  41221  dvdsexpnn0  41227  nn0addcom  41319  nn0mulcom  41323  zmulcomlem  41324  fzsplit1nn0  41477  pell1qrgaplem  41596  monotoddzzfi  41666  jm2.22  41719  jm2.23  41720  rmydioph  41738  expdioph  41747  rp-isfinite6  42254  relexpss1d  42441  relexpmulg  42446  iunrelexpmin2  42448  relexp0a  42452  relexpxpmin  42453  relexpaddss  42454  wallispilem3  44769  etransclem24  44960  lighneallem3  46261  lighneallem4  46264  nn0o1gt2ALTV  46348  nn0oALTV  46350  ztprmneprm  46976  blennn0elnn  47216  blen1b  47227  nn0sumshdiglem1  47260