Theorem ssfid 9170

Description: A subset of a finite set is finite, deduction version of ssfi 9098. (Contributed by Glauco Siliprandi, 21-Nov-2020.)

Hypotheses

Ref	Expression
ssfid.1	⊢ (𝜑 → 𝐴 ∈ Fin)
ssfid.2	⊢ (𝜑 → 𝐵 ⊆ 𝐴)

Assertion

Ref	Expression
ssfid	⊢ (𝜑 → 𝐵 ∈ Fin)

Proof of Theorem ssfid

Step	Hyp	Ref	Expression
1		ssfid.1	. 2 ⊢ (𝜑 → 𝐴 ∈ Fin)
2		ssfid.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
3		ssfi 9098	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → 𝐵 ∈ Fin)

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3890  Fincfn 8884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5368  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-tr 5194  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-om 7809  df-1o 8396  df-en 8885  df-fin 8888

This theorem is referenced by:  ixpfi  9250  fisuppfi  9275  finnzfsuppd  9277  fsuppunbi  9293  ressuppfi  9299  fsuppmptif  9303  fsuppco2  9307  fsuppcor  9308  marypha1lem  9337  wemapso2lem  9458  cantnfp1lem1  9588  pwfseqlem4  10574  hashbclem  14376  hashf1lem2  14380  phphashd  14390  isercolllem2  15590  isercoll  15592  fsum2dlem  15694  fsumcom2  15698  fsumless  15720  fsumabs  15725  fsumrlim  15735  fsumo1  15736  fsumiun  15745  qshash  15751  incexc  15761  incexc2  15762  fprod2dlem  15904  fprodcom2  15908  dvdsfi  16717  4sqlem11  16884  vdwlem11  16920  ramlb  16948  0ram  16949  ramub1lem1  16955  ramub1lem2  16956  prmgaplem4  16983  isstruct2  17077  lagsubg2  19127  lagsubg  19128  orbsta2  19247  symgbasfi  19312  oddvds2  19499  sylow1lem3  19533  sylow1lem4  19534  sylow1lem5  19535  odcau  19537  pgpssslw  19547  sylow2alem2  19551  sylow2a  19552  sylow2blem1  19553  sylow2blem3  19555  slwhash  19557  fislw  19558  sylow2  19559  sylow3lem1  19560  sylow3lem3  19562  sylow3lem4  19563  sylow3lem6  19565  cyggenod  19817  gsumval3lem2  19839  gsumzadd  19855  gsum2dlem1  19903  gsum2dlem2  19904  gsum2d  19905  gsum2d2lem  19906  dprdfadd  19955  ablfac1eu  20008  pgpfac1lem5  20014  pgpfaclem2  20017  pgpfaclem3  20018  ablfaclem3  20022  prmgrpsimpgd  20049  lcomfsupp  20855  dsmmacl  21698  dsmmsubg  21700  dsmmlss  21701  frlmsslsp  21753  psrbaglecl  21880  psrbagaddcl  21881  psrbagcon  21882  mplcoe5  21996  mhpmulcl  22093  psdmplcl  22106  psdmul  22110  mamures  22340  mdetrlin  22545  mdetrsca  22546  mdetralt  22551  madugsum  22586  fin1aufil  23875  xrge0gsumle  24777  xrge0tsms  24778  fsumcn  24815  rrxcph  25337  rrxmval  25350  i1fadd  25640  i1fmul  25641  i1fmulc  25648  i1fres  25650  mbfi1fseqlem4  25663  itgfsum  25772  dvmptfsum  25920  jensenlem1  26937  jensenlem2  26938  jensen  26939  sgmf  27095  sgmnncl  27097  fsumdvdsdiag  27134  fsumdvdscom  27135  dvdsflsumcom  27138  musum  27141  musumsum  27142  muinv  27143  fsumdvdsmul  27145  fsumdvdsmulOLD  27147  perfectlem2  27181  dchrfi  27206  rplogsumlem2  27436  rpvmasumlem  27438  dchrvmasumlem1  27446  dchrisum0ff  27458  dchrisum0  27471  vmalogdivsum2  27489  logsqvma  27493  selberg  27499  selberg34r  27522  pntsval2  27527  pntrlog2bndlem1  27528  onsfi  28336  wwlksnfi  29963  wspthnfi  29976  wspthnonfi  29979  clwwlknfi  30104  qerclwwlknfi  30132  clwlknon2num  30427  numclwlk1lem2  30429  fsuppinisegfi  32749  offinsupp1  32788  hashpss  32872  fsumiunle  32893  elrgspnlem2  33309  elrgspnlem4  33311  elrgspnsubrunlem2  33314  domnprodeq0  33342  elrspunidl  33493  elrspunsn  33494  rprmdvdsprod  33599  deg1prod  33648  psrgsum  33697  psrmonprod  33701  esplyfval2  33714  esplymhp  33717  esplyind  33724  esplyindfv  33725  esplyfvn  33726  vieta  33729  exsslsb  33746  fedgmullem1  33779  fldextrspunlsplem  33823  constrfin  33896  hashreprin  34770  reprfi2  34773  hgt750lema  34807  tgoldbachgtde  34810  aks4d1p4  42510  aks4d1p5  42511  aks4d1p7  42514  aks4d1p8  42518  evl1gprodd  42548  hashscontpowcl  42551  idomnnzgmulnz  42564  deg1gprod  42571  sticksstones3  42579  sticksstones22  42599  aks6d1c6lem5  42608  grpods  42625  unitscyglem1  42626  unitscyglem2  42627  unitscyglem4  42629  unitscyglem5  42630  selvvvval  43017  cantnfub  43752  naddcnff  43793  fprodcnlem  46033  cnrefiisplem  46261  dvmptfprod  46377  dvnprodlem1  46378  sge0uzfsumgt  46876  hoidmvlelem1  47027  hoidmvlelem2  47028  hoidmvlelem3  47029  hoidmvlelem4  47030  hspmbllem1  47058