Theorem ssfid 9173

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3902  Fincfn 8887

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 5242  ax-nul 5252  ax-pr 5378  ax-un 7682

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 3062  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-tr 5207  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-om 7811  df-1o 8399  df-en 8888  df-fin 8891

This theorem is referenced by:  ixpfi  9253  fisuppfi  9278  finnzfsuppd  9280  fsuppunbi  9296  ressuppfi  9302  fsuppmptif  9306  fsuppco2  9310  fsuppcor  9311  marypha1lem  9340  wemapso2lem  9461  cantnfp1lem1  9591  pwfseqlem4  10577  hashbclem  14379  hashf1lem2  14383  phphashd  14393  isercolllem2  15593  isercoll  15595  fsum2dlem  15697  fsumcom2  15701  fsumless  15723  fsumabs  15728  fsumrlim  15738  fsumo1  15739  fsumiun  15748  qshash  15754  incexc  15764  incexc2  15765  fprod2dlem  15907  fprodcom2  15911  dvdsfi  16720  4sqlem11  16887  vdwlem11  16923  ramlb  16951  0ram  16952  ramub1lem1  16958  ramub1lem2  16959  prmgaplem4  16986  isstruct2  17080  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  20857  dsmmacl  21700  dsmmsubg  21702  dsmmlss  21703  frlmsslsp  21755  psrbaglecl  21883  psrbagaddcl  21884  psrbagcon  21885  mplcoe5  21999  mhpmulcl  22096  psdmplcl  22109  psdmul  22113  mamures  22345  mdetrlin  22550  mdetrsca  22551  mdetralt  22556  madugsum  22591  fin1aufil  23880  xrge0gsumle  24782  xrge0tsms  24783  fsumcn  24821  rrxcph  25352  rrxmval  25365  i1fadd  25656  i1fmul  25657  i1fmulc  25664  i1fres  25666  mbfi1fseqlem4  25679  itgfsum  25788  dvmptfsum  25939  jensenlem1  26957  jensenlem2  26958  jensen  26959  sgmf  27115  sgmnncl  27117  fsumdvdsdiag  27154  fsumdvdscom  27155  dvdsflsumcom  27158  musum  27161  musumsum  27162  muinv  27163  fsumdvdsmul  27165  fsumdvdsmulOLD  27167  perfectlem2  27201  dchrfi  27226  rplogsumlem2  27456  rpvmasumlem  27458  dchrvmasumlem1  27466  dchrisum0ff  27478  dchrisum0  27491  vmalogdivsum2  27509  logsqvma  27513  selberg  27519  selberg34r  27542  pntsval2  27547  pntrlog2bndlem1  27548  onsfi  28336  wwlksnfi  29962  wspthnfi  29975  wspthnonfi  29978  clwwlknfi  30103  qerclwwlknfi  30131  clwlknon2num  30426  numclwlk1lem2  30428  fsuppinisegfi  32747  offinsupp1  32786  hashpss  32870  fsumiunle  32891  elrgspnlem2  33306  elrgspnlem4  33308  elrgspnsubrunlem2  33311  domnprodeq0  33339  elrspunidl  33490  elrspunsn  33491  rprmdvdsprod  33596  deg1prod  33645  esplyfval2  33704  esplymhp  33707  esplyind  33712  esplyindfv  33713  esplyfvn  33714  vieta  33717  exsslsb  33734  fedgmullem1  33767  fldextrspunlsplem  33811  constrfin  33884  hashreprin  34758  reprfi2  34761  hgt750lema  34795  tgoldbachgtde  34798  aks4d1p4  42370  aks4d1p5  42371  aks4d1p7  42374  aks4d1p8  42378  evl1gprodd  42408  hashscontpowcl  42411  idomnnzgmulnz  42424  deg1gprod  42431  sticksstones3  42439  sticksstones22  42459  aks6d1c6lem5  42468  grpods  42485  unitscyglem1  42486  unitscyglem2  42487  unitscyglem4  42489  unitscyglem5  42490  selvvvval  42864  cantnfub  43599  naddcnff  43640  fprodcnlem  45881  cnrefiisplem  46109  dvmptfprod  46225  dvnprodlem1  46226  sge0uzfsumgt  46724  hoidmvlelem1  46875  hoidmvlelem2  46876  hoidmvlelem3  46877  hoidmvlelem4  46878  hspmbllem1  46906