Theorem nnssz 12642

Description: Positive integers are a subset of integers. (Contributed by NM, 9-Jan-2002.)

Assertion

Ref	Expression
nnssz	⊢ ℕ ⊆ ℤ

Proof of Theorem nnssz

Step	Hyp	Ref	Expression
1		nnz 12641	. 2 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ ℤ)
2	1	ssriv 3995	1 ⊢ ℕ ⊆ ℤ

Syntax hints:   ⊆ wss 3959  ℕcn 12274  ℤcz 12620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-sep 5307  ax-nul 5314  ax-pr 5437  ax-un 7751  ax-1cn 11223  ax-icn 11224  ax-addcl 11225  ax-addrcl 11226  ax-mulcl 11227  ax-mulrcl 11228  ax-i2m1 11233  ax-1ne0 11234  ax-rrecex 11237  ax-cnre 11238

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-ral 3055  df-rex 3064  df-reu 3374  df-rab 3429  df-v 3474  df-sbc 3789  df-csb 3905  df-dif 3962  df-un 3964  df-in 3966  df-ss 3976  df-pss 3979  df-nul 4336  df-if 4537  df-pw 4612  df-sn 4637  df-pr 4639  df-op 4643  df-uni 4919  df-iun 5008  df-br 5157  df-opab 5219  df-mpt 5240  df-tr 5274  df-id 5584  df-eprel 5590  df-po 5598  df-so 5599  df-fr 5641  df-we 5643  df-xp 5692  df-rel 5693  df-cnv 5694  df-co 5695  df-dm 5696  df-rn 5697  df-res 5698  df-ima 5699  df-pred 6317  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6510  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-ov 7433  df-om 7885  df-2nd 8012  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-neg 11504  df-nn 12275  df-z 12621

This theorem is referenced by:  nn0ssz  12643  nnzOLD  12644  nnzi  12648  zmin  12990  nnssq  13004  divcnvshft  15880  znnen  16235  nthruc  16275  alzdvds  16343  evennn2n  16374  lcmfnnval  16646  lcmfnncl  16651  pclem  16861  prmreclem1  16939  ftalem5  27128  2sqreunnltblem  27503  archiabllem1b  33098  reprsuc  34519  divcnvlin  35622  aks6d1c2  41896  aks6d1c6lem5  41943  aks6d1c7lem1  41946  diophin  42520  hashnzfzclim  44087