Theorem ssfid 9301

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3951  Fincfn 8985

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-om 7888  df-1o 8506  df-en 8986  df-fin 8989

This theorem is referenced by:  ixpfi  9389  fisuppfi  9411  finnzfsuppd  9413  fsuppunbi  9429  ressuppfi  9435  fsuppmptif  9439  fsuppco2  9443  fsuppcor  9444  marypha1lem  9473  wemapso2lem  9592  cantnfp1lem1  9718  pwfseqlem4  10702  hashbclem  14491  hashf1lem2  14495  phphashd  14505  isercolllem2  15702  isercoll  15704  fsum2dlem  15806  fsumcom2  15810  fsumless  15832  fsumabs  15837  fsumrlim  15847  fsumo1  15848  fsumiun  15857  qshash  15863  incexc  15873  incexc2  15874  fprod2dlem  16016  fprodcom2  16020  dvdsfi  16826  4sqlem11  16993  vdwlem11  17029  ramlb  17057  0ram  17058  ramub1lem1  17064  ramub1lem2  17065  prmgaplem4  17092  isstruct2  17186  lagsubg2  19212  lagsubg  19213  orbsta2  19332  symgbasfi  19396  oddvds2  19584  sylow1lem3  19618  sylow1lem4  19619  sylow1lem5  19620  odcau  19622  pgpssslw  19632  sylow2alem2  19636  sylow2a  19637  sylow2blem1  19638  sylow2blem3  19640  slwhash  19642  fislw  19643  sylow2  19644  sylow3lem1  19645  sylow3lem3  19647  sylow3lem4  19648  sylow3lem6  19650  cyggenod  19902  gsumval3lem2  19924  gsumzadd  19940  gsum2dlem1  19988  gsum2dlem2  19989  gsum2d  19990  gsum2d2lem  19991  dprdfadd  20040  ablfac1eu  20093  pgpfac1lem5  20099  pgpfaclem2  20102  pgpfaclem3  20103  ablfaclem3  20107  prmgrpsimpgd  20134  lcomfsupp  20900  dsmmacl  21761  dsmmsubg  21763  dsmmlss  21764  frlmsslsp  21816  psrbaglecl  21943  psrbagaddcl  21944  psrbagcon  21945  mplcoe5  22058  mhpmulcl  22153  psdmplcl  22166  psdmul  22170  mamures  22401  mdetrlin  22608  mdetrsca  22609  mdetralt  22614  madugsum  22649  fin1aufil  23940  xrge0gsumle  24855  xrge0tsms  24856  fsumcn  24894  rrxcph  25426  rrxmval  25439  i1fadd  25730  i1fmul  25731  i1fmulc  25738  i1fres  25740  mbfi1fseqlem4  25753  itgfsum  25862  dvmptfsum  26013  jensenlem1  27030  jensenlem2  27031  jensen  27032  sgmf  27188  sgmnncl  27190  fsumdvdsdiag  27227  fsumdvdscom  27228  dvdsflsumcom  27231  musum  27234  musumsum  27235  muinv  27236  fsumdvdsmul  27238  fsumdvdsmulOLD  27240  perfectlem2  27274  dchrfi  27299  rplogsumlem2  27529  rpvmasumlem  27531  dchrvmasumlem1  27539  dchrisum0ff  27551  dchrisum0  27564  vmalogdivsum2  27582  logsqvma  27586  selberg  27592  selberg34r  27615  pntsval2  27620  pntrlog2bndlem1  27621  wwlksnfi  29926  wspthnfi  29939  wspthnonfi  29942  clwwlknfi  30064  qerclwwlknfi  30092  clwlknon2num  30387  numclwlk1lem2  30389  fsuppinisegfi  32696  offinsupp1  32738  hashpss  32813  fsumiunle  32831  elrgspnlem2  33247  elrgspnlem4  33249  elrgspnsubrunlem2  33252  elrspunidl  33456  elrspunsn  33457  rprmdvdsprod  33562  exsslsb  33647  fedgmullem1  33680  fldextrspunlsplem  33723  constrfin  33787  hashreprin  34635  reprfi2  34638  hgt750lema  34672  tgoldbachgtde  34675  aks4d1p4  42080  aks4d1p5  42081  aks4d1p7  42084  aks4d1p8  42088  evl1gprodd  42118  hashscontpowcl  42121  idomnnzgmulnz  42134  deg1gprod  42141  sticksstones3  42149  sticksstones22  42169  aks6d1c6lem5  42178  grpods  42195  unitscyglem1  42196  unitscyglem2  42197  unitscyglem4  42199  unitscyglem5  42200  selvvvval  42595  cantnfub  43334  naddcnff  43375  fprodcnlem  45614  cnrefiisplem  45844  dvmptfprod  45960  dvnprodlem1  45961  sge0uzfsumgt  46459  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvlelem4  46613  hspmbllem1  46641