Theorem nnnn0 9572

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 9568	. 2 ⊢ ℕ ⊆ ℕ0
2	1	sseli 3244	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℕcn 9305  ℕ₀cn0 9565

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-n0 9566

This theorem is used by:  nnnn0i  9573  elnnnn0b  9609  elnnnn0c  9610  elnn0z  9659  elz2  9718  nn0ind-raph  9765  zindd  9766  fzo1fzo0n0  10597  ubmelfzo  10620  elfzom1elp1fzo  10622  fzo0sn0fzo1  10641  modqmulnn  10781  expnegap0  10986  expcllem  10989  expcl2lemap  10990  expap0  11008  expeq0  11009  mulexpzap  11018  expnlbnd  11104  apexp1  11158  facdiv  11178  faclbnd  11181  faclbnd3  11183  faclbnd6  11184  pfxn0  11462  resqrexlemlo  11781  absexpzap  11848  nnf1o  12145  summodclem2a  12150  fsum3  12156  arisum  12267  expcnvap0  12271  expcnv  12273  geo2sum  12283  geo2lim  12285  geoisum1c  12289  0.999...  12290  mertenslem2  12305  fprodseq  12352  fprodfac  12384  ef0lem  12429  ege2le3  12440  efaddlem  12443  efexp  12451  dvdsmodexp  12564  nn0enne  12671  nnehalf  12673  nno  12675  nn0o  12676  divalg2  12695  ndvdssub  12699  gcddiv  12798  gcdmultiple  12799  gcdmultiplez  12800  rpmulgcd  12805  rplpwr  12806  dvdssqlem  12809  eucalgf  12835  1nprm  12894  isprm6  12927  prmdvdsexp  12928  pw2dvds  12946  oddpwdc  12954  phicl2  12994  phibndlem  12996  phiprmpw  13002  crth  13004  hashgcdlem  13018  phisum  13021  pythagtriplem10  13050  pythagtriplem6  13051  pythagtriplem7  13052  pythagtriplem12  13056  pythagtriplem14  13058  pclemub  13068  pcexp  13090  pcid  13105  pcprod  13127  pcbc  13132  prmpwdvds  13136  infpnlem1  13140  infpnlem2  13141  prmunb  13143  1arith  13148  ennnfonelemjn  13295  ghmmulg  14061  znf1o  14988  znfi  14992  znhash  14993  znidom  14994  znidomb  14995  znrrg  14997  dvexp  15814  plycolemc  15861  logbgcd1irr  16075  birthdaylem2  16094  birthdaylem3  16095  pellexlem1  16097  1sgm2ppw  16115  pcbcctr  16123  bclbnd  16127  lgsval4a  16153  gausslemma2dlem0c  16182  gausslemma2dlem0d  16183  gausslemma2dlem6  16198  2lgslem1a1  16217  2lgslem1c  16221  2lgslem3a1  16228  2lgslem3b1  16229  2lgslem3c1  16230  2lgslem3d1  16231  isclwwlknx  16669