Theorem nnnn0 8778

Description: A positive integer is a nonnegative integer. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
nnnn0	⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)

Proof of Theorem nnnn0

Step	Hyp	Ref	Expression
1		nnssnn0 8774	. 2 ⊢ ℕ ⊆ ℕ0
2	1	sseli 3035	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 1445  ℕcn 8520  ℕ₀cn0 8771

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-v 2635  df-un 3017  df-in 3019  df-ss 3026  df-n0 8772

This theorem is referenced by:  nnnn0i  8779  elnnnn0b  8815  elnnnn0c  8816  elnn0z  8861  elz2  8916  nn0ind-raph  8962  zindd  8963  fzo1fzo0n0  9743  ubmelfzo  9760  elfzom1elp1fzo  9762  fzo0sn0fzo1  9781  modqmulnn  9898  expnegap0  10078  expcllem  10081  expcl2lemap  10082  expap0  10100  expeq0  10101  mulexpzap  10110  expnlbnd  10193  facdiv  10261  faclbnd  10264  faclbnd3  10266  faclbnd6  10267  resqrexlemlo  10561  absexpzap  10628  isummolemnm  10922  summodclem2a  10924  fsum3  10930  arisum  11041  expcnvap0  11045  expcnv  11047  geo2sum  11057  geo2lim  11059  geoisum1c  11063  0.999...  11064  mertenslem2  11079  ef0lem  11099  ege2le3  11110  efaddlem  11113  efexp  11121  nn0enne  11329  nnehalf  11331  nno  11333  nn0o  11334  divalg2  11353  ndvdssub  11357  gcddiv  11435  gcdmultiple  11436  gcdmultiplez  11437  rpmulgcd  11442  rplpwr  11443  dvdssqlem  11446  eucalgf  11464  1nprm  11523  isprm6  11553  prmdvdsexp  11554  pw2dvds  11571  oddpwdc  11579  phicl2  11617  phibndlem  11619  phiprmpw  11625  crth  11627  hashgcdlem  11630