Theorem ssfid 9168

Description: A subset of a finite set is finite, deduction version of ssfi 9096. (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 9096	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → 𝐵 ∈ Fin)

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3885  Fincfn 8882

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 2184  ax-ext 2707  ax-sep 5220  ax-nul 5230  ax-pr 5364  ax-un 7678

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 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2931  df-ral 3050  df-rex 3060  df-reu 3341  df-rab 3388  df-v 3429  df-sbc 3726  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-pss 3905  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-opab 5137  df-tr 5182  df-id 5515  df-eprel 5520  df-po 5528  df-so 5529  df-fr 5573  df-we 5575  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-ord 6315  df-on 6316  df-lim 6317  df-suc 6318  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-om 7807  df-1o 8394  df-en 8883  df-fin 8886

This theorem is referenced by:  ixpfi  9248  fisuppfi  9273  finnzfsuppd  9275  fsuppunbi  9291  ressuppfi  9297  fsuppmptif  9301  fsuppco2  9305  fsuppcor  9306  marypha1lem  9335  wemapso2lem  9456  cantnfp1lem1  9588  pwfseqlem4  10574  hashbclem  14403  hashf1lem2  14407  phphashd  14417  isercolllem2  15617  isercoll  15619  fsum2dlem  15721  fsumcom2  15725  fsumless  15748  fsumabs  15753  fsumrlim  15763  fsumo1  15764  fsumiun  15773  qshash  15779  incexc  15791  incexc2  15792  fprod2dlem  15934  fprodcom2  15938  dvdsfi  16748  4sqlem11  16915  vdwlem11  16951  ramlb  16979  0ram  16980  ramub1lem1  16986  ramub1lem2  16987  prmgaplem4  17014  isstruct2  17108  lagsubg2  19158  lagsubg  19159  orbsta2  19278  symgbasfi  19343  oddvds2  19530  sylow1lem3  19564  sylow1lem4  19565  sylow1lem5  19566  odcau  19568  pgpssslw  19578  sylow2alem2  19582  sylow2a  19583  sylow2blem1  19584  sylow2blem3  19586  slwhash  19588  fislw  19589  sylow2  19590  sylow3lem1  19591  sylow3lem3  19593  sylow3lem4  19594  sylow3lem6  19596  cyggenod  19848  gsumval3lem2  19870  gsumzadd  19886  gsum2dlem1  19934  gsum2dlem2  19935  gsum2d  19936  gsum2d2lem  19937  dprdfadd  19986  ablfac1eu  20039  pgpfac1lem5  20045  pgpfaclem2  20048  pgpfaclem3  20049  ablfaclem3  20053  prmgrpsimpgd  20080  lcomfsupp  20886  dsmmacl  21710  dsmmsubg  21712  dsmmlss  21713  frlmsslsp  21765  psrbaglecl  21892  psrbagaddcl  21893  psrbagcon  21894  mplcoe5  22007  mhpmulcl  22104  psdmplcl  22117  psdmul  22121  mamures  22350  mdetrlin  22555  mdetrsca  22556  mdetralt  22561  madugsum  22596  fin1aufil  23885  xrge0gsumle  24787  xrge0tsms  24788  fsumcn  24825  rrxcph  25347  rrxmval  25360  i1fadd  25650  i1fmul  25651  i1fmulc  25658  i1fres  25660  mbfi1fseqlem4  25673  itgfsum  25782  dvmptfsum  25930  jensenlem1  26938  jensenlem2  26939  jensen  26940  sgmf  27096  sgmnncl  27098  fsumdvdsdiag  27135  fsumdvdscom  27136  dvdsflsumcom  27139  musum  27142  musumsum  27143  muinv  27144  fsumdvdsmul  27146  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  29962  wspthnfi  29975  wspthnonfi  29978  clwwlknfi  30103  qerclwwlknfi  30131  clwlknon2num  30426  numclwlk1lem2  30428  fsuppinisegfi  32748  offinsupp1  32787  hashpss  32870  fsumiunle  32890  elrgspnlem2  33292  elrgspnlem4  33294  elrgspnsubrunlem2  33297  domnprodeq0  33325  elrspunidl  33476  elrspunsn  33477  rprmdvdsprod  33582  deg1prod  33631  psrgsum  33680  psrmonprod  33684  esplyfval2  33697  esplymhp  33700  esplyind  33707  esplyindfv  33708  esplyfvn  33709  vieta  33712  exsslsb  33729  fedgmullem1  33761  fldextrspunlsplem  33805  constrfin  33878  hashreprin  34752  reprfi2  34755  hgt750lema  34789  tgoldbachgtde  34792  aks4d1p4  42506  aks4d1p5  42507  aks4d1p7  42510  aks4d1p8  42514  evl1gprodd  42544  hashscontpowcl  42547  idomnnzgmulnz  42560  deg1gprod  42567  sticksstones3  42575  sticksstones22  42595  aks6d1c6lem5  42604  grpods  42621  unitscyglem1  42622  unitscyglem2  42623  unitscyglem4  42625  unitscyglem5  42626  selvvvval  43006  cantnfub  43737  naddcnff  43778  fprodcnlem  46017  cnrefiisplem  46245  dvmptfprod  46361  dvnprodlem1  46362  sge0uzfsumgt  46860  hoidmvlelem1  47011  hoidmvlelem2  47012  hoidmvlelem3  47013  hoidmvlelem4  47014  hspmbllem1  47042