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  10094  expcllem  10097  expcl2lemap  10098  expap0  10116  expeq0  10117  mulexpzap  10126  expnlbnd  10209  facdiv  10277  faclbnd  10280  faclbnd3  10282  faclbnd6  10283  resqrexlemlo  10577  absexpzap  10644  isummolemnm  10937  summodclem2a  10939  fsum3  10945  arisum  11056  expcnvap0  11060  expcnv  11062  geo2sum  11072  geo2lim  11074  geoisum1c  11078  0.999...  11079  mertenslem2  11094  ef0lem  11114  ege2le3  11125  efaddlem  11128  efexp  11136  nn0enne  11344  nnehalf  11346  nno  11348  nn0o  11349  divalg2  11368  ndvdssub  11372  gcddiv  11450  gcdmultiple  11451  gcdmultiplez  11452  rpmulgcd  11457  rplpwr  11458  dvdssqlem  11461  eucalgf  11479  1nprm  11538  isprm6  11568  prmdvdsexp  11569  pw2dvds  11586  oddpwdc  11594  phicl2  11632  phibndlem  11634  phiprmpw  11640  crth  11642  hashgcdlem  11645