Theorem ssfid 9329

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3976  Fincfn 9003

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-om 7904  df-1o 8522  df-en 9004  df-fin 9007

This theorem is referenced by:  ixpfi  9419  fisuppfi  9441  fsuppunbi  9458  ressuppfi  9464  fsuppmptif  9468  fsuppco2  9472  fsuppcor  9473  marypha1lem  9502  wemapso2lem  9621  cantnfp1lem1  9747  pwfseqlem4  10731  hashbclem  14501  hashf1lem2  14505  phphashd  14515  isercolllem2  15714  isercoll  15716  fsum2dlem  15818  fsumcom2  15822  fsumless  15844  fsumabs  15849  fsumrlim  15859  fsumo1  15860  fsumiun  15869  qshash  15875  incexc  15885  incexc2  15886  fprod2dlem  16028  fprodcom2  16032  4sqlem11  17002  vdwlem11  17038  ramlb  17066  0ram  17067  ramub1lem1  17073  ramub1lem2  17074  prmgaplem4  17101  isstruct2  17196  lagsubg2  19234  lagsubg  19235  orbsta2  19354  symgbasfi  19420  oddvds2  19608  sylow1lem3  19642  sylow1lem4  19643  sylow1lem5  19644  odcau  19646  pgpssslw  19656  sylow2alem2  19660  sylow2a  19661  sylow2blem1  19662  sylow2blem3  19664  slwhash  19666  fislw  19667  sylow2  19668  sylow3lem1  19669  sylow3lem3  19671  sylow3lem4  19672  sylow3lem6  19674  cyggenod  19926  gsumval3lem2  19948  gsumzadd  19964  gsum2dlem1  20012  gsum2dlem2  20013  gsum2d  20014  gsum2d2lem  20015  dprdfadd  20064  ablfac1eu  20117  pgpfac1lem5  20123  pgpfaclem2  20126  pgpfaclem3  20127  ablfaclem3  20131  prmgrpsimpgd  20158  lcomfsupp  20922  dsmmacl  21784  dsmmsubg  21786  dsmmlss  21787  frlmsslsp  21839  psrbaglecl  21966  psrbagaddcl  21967  psrbagcon  21968  mplcoe5  22081  mhpmulcl  22176  psdmplcl  22189  psdmul  22193  mamures  22422  mdetrlin  22629  mdetrsca  22630  mdetralt  22635  madugsum  22670  fin1aufil  23961  xrge0gsumle  24874  xrge0tsms  24875  fsumcn  24913  rrxcph  25445  rrxmval  25458  i1fadd  25749  i1fmul  25750  i1fmulc  25758  i1fres  25760  mbfi1fseqlem4  25773  itgfsum  25882  dvmptfsum  26033  jensenlem1  27048  jensenlem2  27049  jensen  27050  0sgm  27205  sgmf  27206  sgmnncl  27208  fsumdvdsdiag  27245  fsumdvdscom  27246  dvdsflsumcom  27249  musum  27252  musumsum  27253  muinv  27254  fsumdvdsmul  27256  fsumdvdsmulOLD  27258  vmasum  27278  perfectlem2  27292  dchrfi  27317  rplogsumlem2  27547  rpvmasumlem  27549  dchrvmasumlem1  27557  dchrisum0ff  27569  dchrisum0  27582  vmalogdivsum2  27600  logsqvma  27604  logsqvma2  27605  selberg  27610  selberg34r  27633  pntsval2  27638  pntrlog2bndlem1  27639  wwlksnfi  29939  wspthnfi  29952  wspthnonfi  29955  clwwlknfi  30077  qerclwwlknfi  30105  clwlknon2num  30400  numclwlk1lem2  30402  fsuppinisegfi  32699  offinsupp1  32741  fsumiunle  32833  elrspunidl  33421  elrspunsn  33422  rprmdvdsprod  33527  fedgmullem1  33642  constrfin  33736  hashreprin  34597  reprfi2  34600  hgt750lema  34634  tgoldbachgtde  34637  aks4d1p4  42036  aks4d1p5  42037  aks4d1p7  42040  aks4d1p8  42044  evl1gprodd  42074  hashscontpowcl  42077  idomnnzgmulnz  42090  deg1gprod  42097  sticksstones3  42105  sticksstones22  42125  aks6d1c6lem5  42134  grpods  42151  unitscyglem1  42152  unitscyglem2  42153  unitscyglem4  42155  unitscyglem5  42156  selvvvval  42540  cantnfub  43283  naddcnff  43324  finnzfsuppd  44171  fprodcnlem  45520  cnrefiisplem  45750  sge0uzfsumgt  46365  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvlelem4  46519  hspmbllem1  46547