Theorem elnn0 12378

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 12377	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2823	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4098	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11101	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4613	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 912	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 297	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 206   ∨ wo 847   = wceq 1541   ∈ wcel 2111   ∪ cun 3895  {csn 4571  0cc0 11001  ℕcn 12120  ℕ₀cn0 12376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-1cn 11059  ax-icn 11060  ax-addcl 11061  ax-mulcl 11063  ax-i2m1 11069

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-sn 4572  df-n0 12377

This theorem is referenced by:  0nn0  12391  nn0ge0  12401  nnnn0addcl  12406  nnm1nn0  12417  elnnnn0b  12420  nn0sub  12426  elnn0z  12476  elznn0nn  12477  elznn0  12478  elznn  12479  nn0lt10b  12530  nn0ind-raph  12568  nn0ledivnn  13000  expp1  13970  expneg  13971  expcllem  13974  znsqcld  14064  facp1  14180  faclbnd  14192  faclbnd3  14194  faclbnd4lem1  14195  faclbnd4lem3  14197  faclbnd4  14199  bcn1  14215  bcval5  14220  hashv01gt1  14247  hashnncl  14268  seqcoll2  14367  relexpsucl  14933  relexpsucr  14934  relexpcnv  14937  relexprelg  14940  relexpdmg  14944  relexprng  14948  relexpfld  14951  relexpaddg  14955  fz1f1o  15612  arisum  15762  arisum2  15763  pwdif  15770  geomulcvg  15778  fprodfac  15875  ef0lem  15980  nn0enne  16283  nn0o1gt2  16287  bezoutlem3  16447  dfgcd2  16452  mulgcd  16454  nn0rppwr  16467  nn0expgcd  16470  eucalgf  16489  eucalginv  16490  eucalglt  16491  prmdvdsexpr  16623  rpexp1i  16629  nn0gcdsq  16658  odzdvds  16702  pceq0  16778  fldivp1  16804  pockthg  16813  1arith  16834  4sqlem17  16868  4sqlem19  16870  vdwmc2  16886  vdwlem13  16900  0ram  16927  ram0  16929  ramz  16932  ramcl  16936  ressmulgnn0  18985  mulgnn0gsum  18988  mulgnn0p1  18993  mulgnn0subcl  18995  mulgneg  19000  mulgnn0z  19009  mulgnn0dir  19012  mulgnn0ass  19018  submmulg  19026  odcl  19443  mndodcongi  19450  oddvdsnn0  19451  odnncl  19452  oddvds  19454  dfod2  19471  odcl2  19472  gexcl  19487  gexdvds  19491  gexnnod  19495  sylow1lem1  19505  mulgnn0di  19732  torsubg  19761  ablfac1eu  19982  gzrngunitlem  21364  zringlpirlem3  21396  prmirredlem  21404  prmirred  21406  znf1o  21483  evlslem3  22010  dscmet  24482  dvexp2  25880  tdeglem4  25987  dgrnznn  26174  coefv0  26175  dgreq0  26193  dgrcolem2  26202  dvply1  26213  aaliou2  26270  radcnv0  26347  logfac  26532  logtayl  26591  cxpexp  26599  birthdaylem2  26884  harmonicbnd3  26940  sqf11  27071  ppiltx  27109  sqff1o  27114  lgsdir  27265  lgsabs1  27269  lgseisenlem1  27308  2sqlem7  27357  2sqblem  27364  2sqnn  27372  chebbnd1lem1  27402  nexple  32819  xrsmulgzz  32982  ressmulgnn0d  33017  fldext2rspun  33687  eulerpartlemsv2  34363  eulerpartlemv  34369  eulerpartlemb  34373  eulerpartlemf  34375  eulerpartlemgvv  34381  eulerpartlemgh  34383  fz0n  35767  bccolsum  35775  nn0prpw  36357  aks4d1p1  42109  sticksstones13  42192  negn0nposznnd  42315  dvdsexpnn0  42367  nn0addcom  42495  nn0mulcom  42499  zmulcomlem  42500  fsuppind  42623  fzsplit1nn0  42787  pell1qrgaplem  42906  monotoddzzfi  42975  jm2.22  43028  jm2.23  43029  rmydioph  43047  expdioph  43056  rp-isfinite6  43551  relexpss1d  43738  relexpmulg  43743  iunrelexpmin2  43745  relexp0a  43749  relexpxpmin  43750  relexpaddss  43751  wallispilem3  46105  etransclem24  46296  lighneallem3  47638  lighneallem4  47641  nn0o1gt2ALTV  47725  nn0oALTV  47727  ztprmneprm  48378  blennn0elnn  48609  blen1b  48620  nn0sumshdiglem1  48653