Theorem nnnn0d 8341

Description: A positive integer is a nonnegative integer. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nnnn0d.1	⊢ (𝜑 → 𝐴 ∈ ℕ)

Assertion

Ref	Expression
nnnn0d	⊢ (𝜑 → 𝐴 ∈ ℕ0)

Proof of Theorem nnnn0d

Step	Hyp	Ref	Expression
1		nnssnn0 8291	. 2 ⊢ ℕ ⊆ ℕ0
2		nnnn0d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sseldi 2997	1 ⊢ (𝜑 → 𝐴 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 1433  ℕcn 8039  ℕ₀cn0 8288

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-v 2603  df-un 2977  df-in 2979  df-ss 2986  df-n0 8289

This theorem is referenced by:  nn0ge2m1nn0  8349  nnzd  8468  eluzge2nn0  8658  modsumfzodifsn  9398  addmodlteq  9400  expinnval  9479  expgt1  9514  expaddzaplem  9519  expaddzap  9520  expmulzap  9522  expnbnd  9596  facwordi  9667  faclbnd  9668  facavg  9673  bcm1k  9687  ibcval5  9690  resqrexlemnm  9904  resqrexlemcvg  9905  dvdsfac  10260  divalglemnqt  10320  divalglemeunn  10321  gcdval  10351  gcdcl  10358  mulgcd  10405  rplpwr  10416  rppwr  10417  lcmcl  10454  lcmgcdnn  10464  nprmdvds1  10521  rpexp  10532  pw2dvdslemn  10543  sqpweven  10553  2sqpwodd  10554