Theorem ssfid 8898

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

Syntax hints:   → wi 4   ∈ wcel 2110   ⊆ wss 3866  Fincfn 8626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322  ax-un 7523

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3410  df-sbc 3695  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-om 7645  df-1o 8202  df-en 8627  df-fin 8630

This theorem is referenced by:  ixpfi  8973  fisuppfi  8993  fsuppunbi  9006  ressuppfi  9011  fsuppmptif  9015  fsuppco2  9019  fsuppcor  9020  marypha1lem  9049  wemapso2lem  9168  cantnfp1lem1  9293  pwfseqlem4  10276  hashbclem  14016  hashf1lem2  14022  phphashd  14032  isercolllem2  15229  isercoll  15231  fsum2dlem  15334  fsumcom2  15338  fsumless  15360  fsumabs  15365  fsumrlim  15375  fsumo1  15376  fsumiun  15385  qshash  15391  incexc  15401  incexc2  15402  fprod2dlem  15542  fprodcom2  15546  4sqlem11  16508  vdwlem11  16544  ramlb  16572  0ram  16573  ramub1lem1  16579  ramub1lem2  16580  prmgaplem4  16607  isstruct2  16702  lagsubg2  18605  lagsubg  18606  orbsta2  18708  symgbasfi  18771  oddvds2  18957  sylow1lem3  18989  sylow1lem4  18990  sylow1lem5  18991  odcau  18993  pgpssslw  19003  sylow2alem2  19007  sylow2a  19008  sylow2blem1  19009  sylow2blem3  19011  slwhash  19013  fislw  19014  sylow2  19015  sylow3lem1  19016  sylow3lem3  19018  sylow3lem4  19019  sylow3lem6  19021  cyggenod  19268  gsumval3lem2  19291  gsumzadd  19307  gsum2dlem1  19355  gsum2dlem2  19356  gsum2d  19357  gsum2d2lem  19358  dprdfadd  19407  ablfac1eu  19460  pgpfac1lem5  19466  pgpfaclem2  19469  pgpfaclem3  19470  ablfaclem3  19474  prmgrpsimpgd  19501  lcomfsupp  19939  dsmmacl  20703  dsmmsubg  20705  dsmmlss  20706  frlmsslsp  20758  psrbaglecl  20885  psrbagleclOLD  20886  psrbagaddcl  20887  psrbagaddclOLD  20888  psrbagcon  20889  psrbagconOLD  20890  mplcoe5  20997  mhpmulcl  21089  mamures  21289  mdetrlin  21499  mdetrsca  21500  mdetralt  21505  madugsum  21540  fin1aufil  22829  xrge0gsumle  23730  xrge0tsms  23731  fsumcn  23767  rrxcph  24289  rrxmval  24302  i1fadd  24592  i1fmul  24593  i1fmulc  24601  i1fres  24603  mbfi1fseqlem4  24616  itgfsum  24724  dvmptfsum  24872  jensenlem1  25869  jensenlem2  25870  jensen  25871  0sgm  26026  sgmf  26027  sgmnncl  26029  fsumdvdsdiag  26066  fsumdvdscom  26067  dvdsflsumcom  26070  musum  26073  musumsum  26074  muinv  26075  fsumdvdsmul  26077  vmasum  26097  perfectlem2  26111  dchrfi  26136  rplogsumlem2  26366  rpvmasumlem  26368  dchrvmasumlem1  26376  dchrisum0ff  26388  dchrisum0  26401  vmalogdivsum2  26419  logsqvma  26423  logsqvma2  26424  selberg  26429  selberg34r  26452  pntsval2  26457  pntrlog2bndlem1  26458  wwlksnfi  27990  wspthnfi  28003  wspthnonfi  28006  clwwlknfi  28128  qerclwwlknfi  28156  clwlknon2num  28451  numclwlk1lem2  28453  fsuppinisegfi  30741  offinsupp1  30782  fsumiunle  30863  elrspunidl  31320  fedgmullem1  31424  hashreprin  32312  reprfi2  32315  hgt750lema  32349  tgoldbachgtde  32352  sticksstones3  39826  sticksstones22  39846  evlsbagval  39985  mhphf  39995  finnzfsuppd  41498  fprodcnlem  42815  cnrefiisplem  43045  sge0uzfsumgt  43657  hoidmvlelem1  43808  hoidmvlelem2  43809  hoidmvlelem3  43810  hoidmvlelem4  43811  hspmbllem1  43839