Theorem elnn0 12601

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 12600	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
2	1	eleq2i 2853	. 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0}))
3		elun 4100	. 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4		c0ex 11293	. . . 4 ⊢ 0 ∈ V
5	4	elsn2 4626	. . 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 2145   ∪ cun 3897  {csn 4584  0cc0 11193  ℕcn 12328  ℕ₀cn0 12599

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 2147  ax-9 2155  ax-ext 2733  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-mulcl 11255  ax-i2m1 11261

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-sn 4585  df-n0 12600

This theorem is used by:  0nn0  12614  nn0ge0  12624  nnnn0addcl  12629  nnm1nn0  12640  elnnnn0b  12643  nn0sub  12649  elnn0z  12699  elznn0nn  12700  elznn0  12701  elznn  12702  nn0lt10b  12754  nn0ind-raph  12792  nn0ledivnn  13228  expp1  14204  expneg  14205  expcllem  14208  znsqcld  14298  facp1  14415  faclbnd  14427  faclbnd3  14429  faclbnd4lem1  14430  faclbnd4lem3  14432  faclbnd4  14434  bcn1  14450  bcval5  14455  hashv01gt1  14482  hashnncl  14503  seqcoll2  14603  relexpsucl  15177  relexpsucr  15178  relexpcnv  15181  relexprelg  15184  relexpdmg  15188  relexprng  15192  relexpfld  15195  relexpaddg  15199  fz1f1o  15869  arisum  16022  arisum2  16023  pwdif  16030  geomulcvg  16038  fprodfac  16133  ef0lem  16237  nn0enne  16540  nn0o1gt2  16544  bezoutlem3  16707  dfgcd2  16712  mulgcd  16714  nn0rppwr  16728  nn0expgcd  16731  eucalgf  16751  eucalginv  16752  eucalglt  16753  prmdvdsexpr  16886  rpexp1i  16892  nn0gcdsq  16921  odzdvds  16966  pceq0  17042  fldivp1  17068  pockthg  17077  1arith  17098  4sqlem17  17132  4sqlem19  17134  vdwmc2  17150  vdwlem13  17164  0ram  17191  ram0  17193  ramz  17196  ramcl  17200  ressmulgnn0  19280  mulgnn0gsum  19283  mulgnn0p1  19288  mulgnn0subcl  19290  mulgneg  19295  mulgnn0z  19304  mulgnn0dir  19307  mulgnn0ass  19313  submmulg  19321  odcl  19743  mndodcongi  19750  oddvdsnn0  19751  odnncl  19752  oddvds  19754  dfod2  19771  odcl2  19772  gexcl  19787  gexdvds  19791  gexnnod  19795  sylow1lem1  19805  mulgnn0di  20032  torsubg  20061  ablfac1eu  20282  gzrngunitlem  21731  zringlpirlem3  21763  prmirredlem  21771  prmirred  21773  znf1o  21850  evlslem3  22382  dscmet  24884  dvexp2  26267  tdeglem4  26371  dgrnznn  26559  coefv0  26560  dgreq0  26577  dgrcolem2  26586  dvply1  26598  aaliou2  26660  radcnv0  26736  logfac  26922  logtayl  26981  cxpexp  26989  birthdaylem2  27273  harmonicbnd3  27328  sqf11  27459  ppiltx  27497  sqff1o  27502  lgsdir  27652  lgsabs1  27656  lgseisenlem1  27695  2sqlem7  27744  2sqblem  27751  2sqnn  27759  chebbnd1lem1  27789  nexple  33417  xrsmulgzz  33563  ressmulgnn0d  33598  fldext2rspun  34307  eulerpartlemsv2  34983  eulerpartlemv  34989  eulerpartlemb  34993  eulerpartlemf  34995  eulerpartlemgvv  35001  eulerpartlemgh  35003  fz0n  36475  bccolsum  36483  nn0prpw  37091  aks4d1p1  43106  sticksstones13  43189  negn0nposznnd  43319  dvdsexpnn0  43366  nn0addcom  43506  nn0mulcom  43510  zmulcomlem  43511  fsuppind  43598  fzsplit1nn0  43744  pell1qrgaplem  43859  monotoddzzfi  43928  jm2.22  43981  jm2.23  43982  rmydioph  44000  expdioph  44009  rp-isfinite6  44503  relexpss1d  44690  relexpmulg  44695  iunrelexpmin2  44697  relexp0a  44701  relexpxpmin  44702  relexpaddss  44703  wallispilem3  47046  etransclem24  47237  lighneallem3  48661  lighneallem4  48664  nn0o1gt2ALTV  48761  nn0oALTV  48763  ztprmneprm  49428  blennn0elnn  49658  blen1b  49669  nn0sumshdiglem1  49702