Theorem elnn0 12394

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 12393	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2825	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4102	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11117	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4619	. . 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 2113   ∪ cun 3896  {csn 4577  0cc0 11017  ℕcn 12136  ℕ₀cn0 12392

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 2115  ax-9 2123  ax-ext 2705  ax-1cn 11075  ax-icn 11076  ax-addcl 11077  ax-mulcl 11079  ax-i2m1 11085

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 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-sn 4578  df-n0 12393

This theorem is referenced by:  0nn0  12407  nn0ge0  12417  nnnn0addcl  12422  nnm1nn0  12433  elnnnn0b  12436  nn0sub  12442  elnn0z  12492  elznn0nn  12493  elznn0  12494  elznn  12495  nn0lt10b  12545  nn0ind-raph  12583  nn0ledivnn  13011  expp1  13982  expneg  13983  expcllem  13986  znsqcld  14076  facp1  14192  faclbnd  14204  faclbnd3  14206  faclbnd4lem1  14207  faclbnd4lem3  14209  faclbnd4  14211  bcn1  14227  bcval5  14232  hashv01gt1  14259  hashnncl  14280  seqcoll2  14379  relexpsucl  14945  relexpsucr  14946  relexpcnv  14949  relexprelg  14952  relexpdmg  14956  relexprng  14960  relexpfld  14963  relexpaddg  14967  fz1f1o  15624  arisum  15774  arisum2  15775  pwdif  15782  geomulcvg  15790  fprodfac  15887  ef0lem  15992  nn0enne  16295  nn0o1gt2  16299  bezoutlem3  16459  dfgcd2  16464  mulgcd  16466  nn0rppwr  16479  nn0expgcd  16482  eucalgf  16501  eucalginv  16502  eucalglt  16503  prmdvdsexpr  16635  rpexp1i  16641  nn0gcdsq  16670  odzdvds  16714  pceq0  16790  fldivp1  16816  pockthg  16825  1arith  16846  4sqlem17  16880  4sqlem19  16882  vdwmc2  16898  vdwlem13  16912  0ram  16939  ram0  16941  ramz  16944  ramcl  16948  ressmulgnn0  18998  mulgnn0gsum  19001  mulgnn0p1  19006  mulgnn0subcl  19008  mulgneg  19013  mulgnn0z  19022  mulgnn0dir  19025  mulgnn0ass  19031  submmulg  19039  odcl  19456  mndodcongi  19463  oddvdsnn0  19464  odnncl  19465  oddvds  19467  dfod2  19484  odcl2  19485  gexcl  19500  gexdvds  19504  gexnnod  19508  sylow1lem1  19518  mulgnn0di  19745  torsubg  19774  ablfac1eu  19995  gzrngunitlem  21378  zringlpirlem3  21410  prmirredlem  21418  prmirred  21420  znf1o  21497  evlslem3  22026  dscmet  24507  dvexp2  25905  tdeglem4  26012  dgrnznn  26199  coefv0  26200  dgreq0  26218  dgrcolem2  26227  dvply1  26238  aaliou2  26295  radcnv0  26372  logfac  26557  logtayl  26616  cxpexp  26624  birthdaylem2  26909  harmonicbnd3  26965  sqf11  27096  ppiltx  27134  sqff1o  27139  lgsdir  27290  lgsabs1  27294  lgseisenlem1  27333  2sqlem7  27382  2sqblem  27389  2sqnn  27397  chebbnd1lem1  27427  nexple  32853  xrsmulgzz  33019  ressmulgnn0d  33055  fldext2rspun  33767  eulerpartlemsv2  34443  eulerpartlemv  34449  eulerpartlemb  34453  eulerpartlemf  34455  eulerpartlemgvv  34461  eulerpartlemgh  34463  fz0n  35847  bccolsum  35855  nn0prpw  36439  aks4d1p1  42242  sticksstones13  42325  negn0nposznnd  42452  dvdsexpnn0  42504  nn0addcom  42632  nn0mulcom  42636  zmulcomlem  42637  fsuppind  42748  fzsplit1nn0  42911  pell1qrgaplem  43030  monotoddzzfi  43099  jm2.22  43152  jm2.23  43153  rmydioph  43171  expdioph  43180  rp-isfinite6  43675  relexpss1d  43862  relexpmulg  43867  iunrelexpmin2  43869  relexp0a  43873  relexpxpmin  43874  relexpaddss  43875  wallispilem3  46227  etransclem24  46418  lighneallem3  47769  lighneallem4  47772  nn0o1gt2ALTV  47856  nn0oALTV  47858  ztprmneprm  48509  blennn0elnn  48739  blen1b  48750  nn0sumshdiglem1  48783