Theorem elnn0 12517

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 12516	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2857	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4107	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11211	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4633	. . 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 1570   ∈ wcel 2146   ∪ cun 3904  {csn 4591  0cc0 11111  ℕcn 12244  ℕ₀cn0 12515

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-1cn 11169  ax-icn 11170  ax-addcl 11171  ax-mulcl 11173  ax-i2m1 11179

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-sn 4592  df-n0 12516

This theorem is used by:  0nn0  12530  nn0ge0  12540  nnnn0addcl  12545  nnm1nn0  12556  elnnnn0b  12559  nn0sub  12565  elnn0z  12615  elznn0nn  12616  elznn0  12617  elznn  12618  nn0lt10b  12670  nn0ind-raph  12708  nn0ledivnn  13143  expp1  14118  expneg  14119  expcllem  14122  znsqcld  14212  facp1  14328  faclbnd  14340  faclbnd3  14342  faclbnd4lem1  14343  faclbnd4lem3  14345  faclbnd4  14347  bcn1  14363  bcval5  14368  hashv01gt1  14395  hashnncl  14416  seqcoll2  14516  relexpsucl  15088  relexpsucr  15089  relexpcnv  15092  relexprelg  15095  relexpdmg  15099  relexprng  15103  relexpfld  15106  relexpaddg  15110  fz1f1o  15780  arisum  15933  arisum2  15934  pwdif  15941  geomulcvg  15949  fprodfac  16046  ef0lem  16150  nn0enne  16453  nn0o1gt2  16457  bezoutlem3  16617  dfgcd2  16622  mulgcd  16624  nn0rppwr  16637  nn0expgcd  16640  eucalgf  16659  eucalginv  16660  eucalglt  16661  prmdvdsexpr  16794  rpexp1i  16800  nn0gcdsq  16829  odzdvds  16873  pceq0  16949  fldivp1  16975  pockthg  16984  1arith  17005  4sqlem17  17039  4sqlem19  17041  vdwmc2  17057  vdwlem13  17071  0ram  17098  ram0  17100  ramz  17103  ramcl  17107  ressmulgnn0  19167  mulgnn0gsum  19170  mulgnn0p1  19175  mulgnn0subcl  19177  mulgneg  19182  mulgnn0z  19191  mulgnn0dir  19194  mulgnn0ass  19200  submmulg  19208  odcl  19630  mndodcongi  19637  oddvdsnn0  19638  odnncl  19639  oddvds  19641  dfod2  19658  odcl2  19659  gexcl  19674  gexdvds  19678  gexnnod  19682  sylow1lem1  19692  mulgnn0di  19919  torsubg  19948  ablfac1eu  20169  gzrngunitlem  21612  zringlpirlem3  21644  prmirredlem  21652  prmirred  21654  znf1o  21731  evlslem3  22261  dscmet  24760  dvexp2  26144  tdeglem4  26248  dgrnznn  26435  coefv0  26436  dgreq0  26453  dgrcolem2  26462  dvply1  26476  aaliou2  26534  radcnv0  26610  logfac  26797  logtayl  26856  cxpexp  26864  birthdaylem2  27148  harmonicbnd3  27203  sqf11  27334  ppiltx  27372  sqff1o  27377  lgsdir  27527  lgsabs1  27531  lgseisenlem1  27570  2sqlem7  27619  2sqblem  27626  2sqnn  27634  chebbnd1lem1  27664  nexple  33223  xrsmulgzz  33369  ressmulgnn0d  33404  fldext2rspun  34112  eulerpartlemsv2  34789  eulerpartlemv  34795  eulerpartlemb  34799  eulerpartlemf  34801  eulerpartlemgvv  34807  eulerpartlemgh  34809  fz0n  36236  bccolsum  36244  nn0prpw  36867  aks4d1p1  42876  sticksstones13  42959  negn0nposznnd  43076  dvdsexpnn0  43128  nn0addcom  43269  nn0mulcom  43273  zmulcomlem  43274  fsuppind  43355  fzsplit1nn0  43518  pell1qrgaplem  43633  monotoddzzfi  43702  jm2.22  43755  jm2.23  43756  rmydioph  43774  expdioph  43783  rp-isfinite6  44277  relexpss1d  44464  relexpmulg  44469  iunrelexpmin2  44471  relexp0a  44475  relexpxpmin  44476  relexpaddss  44477  wallispilem3  46814  etransclem24  47005  lighneallem3  48392  lighneallem4  48395  nn0o1gt2ALTV  48492  nn0oALTV  48494  ztprmneprm  49160  blennn0elnn  49390  blen1b  49401  nn0sumshdiglem1  49434