Theorem elnn0 12528

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 12527	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2833	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4153	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11255	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4665	. . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0)
6	5	orbi2i 913	. 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
7	2, 3, 6	3bitri 297	1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Syntax hints:   ↔ wb 206   ∨ wo 848   = wceq 1540   ∈ wcel 2108   ∪ cun 3949  {csn 4626  0cc0 11155  ℕcn 12266  ℕ₀cn0 12526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-mulcl 11217  ax-i2m1 11223

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-sn 4627  df-n0 12527

This theorem is referenced by:  0nn0  12541  nn0ge0  12551  nnnn0addcl  12556  nnm1nn0  12567  elnnnn0b  12570  nn0sub  12576  elnn0z  12626  elznn0nn  12627  elznn0  12628  elznn  12629  nn0lt10b  12680  nn0ind-raph  12718  nn0ledivnn  13148  expp1  14109  expneg  14110  expcllem  14113  znsqcld  14202  facp1  14317  faclbnd  14329  faclbnd3  14331  faclbnd4lem1  14332  faclbnd4lem3  14334  faclbnd4  14336  bcn1  14352  bcval5  14357  hashv01gt1  14384  hashnncl  14405  seqcoll2  14504  relexpsucl  15070  relexpsucr  15071  relexpcnv  15074  relexprelg  15077  relexpdmg  15081  relexprng  15085  relexpfld  15088  relexpaddg  15092  fz1f1o  15746  arisum  15896  arisum2  15897  pwdif  15904  geomulcvg  15912  fprodfac  16009  ef0lem  16114  nn0enne  16414  nn0o1gt2  16418  bezoutlem3  16578  dfgcd2  16583  mulgcd  16585  nn0rppwr  16598  nn0expgcd  16601  eucalgf  16620  eucalginv  16621  eucalglt  16622  prmdvdsexpr  16754  rpexp1i  16760  nn0gcdsq  16789  odzdvds  16833  pceq0  16909  fldivp1  16935  pockthg  16944  1arith  16965  4sqlem17  16999  4sqlem19  17001  vdwmc2  17017  vdwlem13  17031  0ram  17058  ram0  17060  ramz  17063  ramcl  17067  ressmulgnn0  19095  mulgnn0gsum  19098  mulgnn0p1  19103  mulgnn0subcl  19105  mulgneg  19110  mulgnn0z  19119  mulgnn0dir  19122  mulgnn0ass  19128  submmulg  19136  odcl  19554  mndodcongi  19561  oddvdsnn0  19562  odnncl  19563  oddvds  19565  dfod2  19582  odcl2  19583  gexcl  19598  gexdvds  19602  gexnnod  19606  sylow1lem1  19616  mulgnn0di  19843  torsubg  19872  ablfac1eu  20093  gzrngunitlem  21450  zringlpirlem3  21475  prmirredlem  21483  prmirred  21485  znf1o  21570  evlslem3  22104  dscmet  24585  dvexp2  25992  tdeglem4  26099  dgrnznn  26286  coefv0  26287  dgreq0  26305  dgrcolem2  26314  dvply1  26325  aaliou2  26382  radcnv0  26459  logfac  26643  logtayl  26702  cxpexp  26710  birthdaylem2  26995  harmonicbnd3  27051  sqf11  27182  ppiltx  27220  sqff1o  27225  lgsdir  27376  lgsabs1  27380  lgseisenlem1  27419  2sqlem7  27468  2sqblem  27475  2sqnn  27483  chebbnd1lem1  27513  nexple  32833  xrsmulgzz  33011  fldext2rspun  33732  eulerpartlemsv2  34360  eulerpartlemv  34366  eulerpartlemb  34370  eulerpartlemf  34372  eulerpartlemgvv  34378  eulerpartlemgh  34380  fz0n  35731  bccolsum  35739  nn0prpw  36324  aks4d1p1  42077  sticksstones13  42160  negn0nposznnd  42317  dvdsexpnn0  42369  nn0addcom  42480  nn0mulcom  42484  zmulcomlem  42485  fsuppind  42600  fzsplit1nn0  42765  pell1qrgaplem  42884  monotoddzzfi  42954  jm2.22  43007  jm2.23  43008  rmydioph  43026  expdioph  43035  rp-isfinite6  43531  relexpss1d  43718  relexpmulg  43723  iunrelexpmin2  43725  relexp0a  43729  relexpxpmin  43730  relexpaddss  43731  wallispilem3  46082  etransclem24  46273  lighneallem3  47594  lighneallem4  47597  nn0o1gt2ALTV  47681  nn0oALTV  47683  ztprmneprm  48263  blennn0elnn  48498  blen1b  48509  nn0sumshdiglem1  48542