Theorem ssfid 9198

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

Syntax hints:   → wi 4   ∈ wcel 2132   ⊆ wss 3895  Fincfn 8912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-sep 5236  ax-nul 5246  ax-pr 5380  ax-un 7703

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-ral 3067  df-rex 3077  df-reu 3358  df-rab 3405  df-v 3446  df-sbc 3736  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-pss 3915  df-nul 4277  df-if 4471  df-pw 4547  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-opab 5153  df-tr 5198  df-id 5531  df-eprel 5536  df-po 5544  df-so 5545  df-fr 5589  df-we 5591  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-res 5648  df-ima 5649  df-ord 6334  df-on 6335  df-lim 6336  df-suc 6337  df-iota 6462  df-fun 6508  df-fn 6509  df-f 6510  df-f1 6511  df-fo 6512  df-f1o 6513  df-fv 6514  df-om 7832  df-1o 8421  df-en 8913  df-fin 8916

This theorem is referenced by:  ixpfi  9278  fisuppfi  9303  finnzfsuppd  9305  fsuppunbi  9321  ressuppfi  9327  fsuppmptif  9331  fsuppco2  9335  fsuppcor  9336  marypha1lem  9365  wemapso2lem  9486  cantnfp1lem1  9619  pwfseqlem4  10606  hashbclem  14451  hashf1lem2  14455  phphashd  14465  isercolllem2  15665  isercoll  15667  fsum2dlem  15769  fsumcom2  15773  fsumless  15796  fsumabs  15801  fsumrlim  15811  fsumo1  15812  fsumiun  15821  qshash  15827  incexc  15839  incexc2  15840  fprod2dlem  15982  fprodcom2  15986  dvdsfi  16796  4sqlem11  16963  vdwlem11  16999  ramlb  17027  0ram  17028  ramub1lem1  17034  ramub1lem2  17035  prmgaplem4  17062  isstruct2  17157  lagsubg2  19207  lagsubg  19208  orbsta2  19326  symgbasfi  19391  oddvds2  19578  sylow1lem3  19612  sylow1lem4  19613  sylow1lem5  19614  odcau  19616  pgpssslw  19626  sylow2alem2  19630  sylow2a  19631  sylow2blem1  19632  sylow2blem3  19634  slwhash  19636  fislw  19637  sylow2  19638  sylow3lem1  19639  sylow3lem3  19641  sylow3lem4  19642  sylow3lem6  19644  cyggenod  19896  gsumval3lem2  19918  gsumzadd  19934  gsum2dlem1  19982  gsum2dlem2  19983  gsum2d  19984  gsum2d2lem  19985  dprdfadd  20034  ablfac1eu  20087  pgpfac1lem5  20093  pgpfaclem2  20096  pgpfaclem3  20097  ablfaclem3  20101  prmgrpsimpgd  20128  lcomfsupp  20938  dsmmacl  21762  dsmmsubg  21764  dsmmlss  21765  frlmsslsp  21817  psrbaglecl  21944  psrbagaddcl  21945  psrbagcon  21946  mplcoe5  22062  selvvvval  22164  mhpmulcl  22183  psdmplcl  22196  psdmul  22200  mamures  22426  mdetrlin  22631  mdetrsca  22632  mdetralt  22637  madugsum  22672  fin1aufil  23961  xrge0gsumle  24863  xrge0tsms  24864  fsumcn  24901  rrxcph  25423  rrxmval  25436  i1fadd  25726  i1fmul  25727  i1fmulc  25734  i1fres  25736  mbfi1fseqlem4  25749  itgfsum  25858  dvmptfsum  26006  jensenlem1  27017  jensenlem2  27018  jensen  27019  sgmf  27175  sgmnncl  27177  fsumdvdsdiag  27214  fsumdvdscom  27215  dvdsflsumcom  27218  musum  27221  musumsum  27222  muinv  27223  fsumdvdsmul  27225  perfectlem2  27260  dchrfi  27285  rplogsumlem2  27515  rpvmasumlem  27517  dchrvmasumlem1  27525  dchrisum0ff  27537  dchrisum0  27550  vmalogdivsum2  27568  logsqvma  27572  selberg  27578  selberg34r  27601  pntsval2  27606  pntrlog2bndlem1  27607  onsfi  28415  wwlksnfi  30041  wspthnfi  30054  wspthnonfi  30057  clwwlknfi  30182  qerclwwlknfi  30210  clwlknon2num  30505  numclwlk1lem2  30507  fsuppinisegfi  32828  offinsupp1  32867  hashpss  32950  fsumiunle  32970  elrgspnlem2  33373  elrgspnlem4  33375  elrgspnsubrunlem2  33378  domnprodeq0  33406  elrspunidl  33560  elrspunsn  33561  rprmdvdsprod  33674  deg1prod  33723  mplidomlem  33768  psrgsum  33789  psrmonprod  33793  esplyfval2  33806  esplymhp  33809  esplyind  33816  esplyindfv  33817  esplyfvn  33818  vieta  33821  exsslsb  33838  fedgmullem1  33870  fldextrspunlsplem  33914  constrfin  33987  hashreprin  34861  reprfi2  34864  hgt750lema  34898  tgoldbachgtde  34901  aks4d1p4  42634  aks4d1p5  42635  aks4d1p7  42638  aks4d1p8  42642  evl1gprodd  42672  hashscontpowcl  42675  idomnnzgmulnz  42688  deg1gprod  42695  sticksstones3  42703  sticksstones22  42723  aks6d1c6lem5  42732  grpods  42749  unitscyglem1  42750  unitscyglem2  42751  unitscyglem4  42753  unitscyglem5  42754  cantnfub  43836  naddcnff  43877  fprodcnlem  46113  cnrefiisplem  46341  dvmptfprod  46457  dvnprodlem1  46458  sge0uzfsumgt  46956  hoidmvlelem1  47107  hoidmvlelem2  47108  hoidmvlelem3  47109  hoidmvlelem4  47110  hspmbllem1  47138