Theorem ssfid 9292

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

Syntax hints:   → wi 4   ∈ wcel 2098   ⊆ wss 3944  Fincfn 8964

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429  ax-un 7741

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-om 7872  df-1o 8487  df-en 8965  df-fin 8968

This theorem is referenced by:  ixpfi  9375  fisuppfi  9397  fsuppunbi  9414  ressuppfi  9420  fsuppmptif  9424  fsuppco2  9428  fsuppcor  9429  marypha1lem  9458  wemapso2lem  9577  cantnfp1lem1  9703  pwfseqlem4  10687  hashbclem  14447  hashf1lem2  14453  phphashd  14463  isercolllem2  15648  isercoll  15650  fsum2dlem  15752  fsumcom2  15756  fsumless  15778  fsumabs  15783  fsumrlim  15793  fsumo1  15794  fsumiun  15803  qshash  15809  incexc  15819  incexc2  15820  fprod2dlem  15960  fprodcom2  15964  4sqlem11  16927  vdwlem11  16963  ramlb  16991  0ram  16992  ramub1lem1  16998  ramub1lem2  16999  prmgaplem4  17026  isstruct2  17121  lagsubg2  19157  lagsubg  19158  orbsta2  19277  symgbasfi  19345  oddvds2  19533  sylow1lem3  19567  sylow1lem4  19568  sylow1lem5  19569  odcau  19571  pgpssslw  19581  sylow2alem2  19585  sylow2a  19586  sylow2blem1  19587  sylow2blem3  19589  slwhash  19591  fislw  19592  sylow2  19593  sylow3lem1  19594  sylow3lem3  19596  sylow3lem4  19597  sylow3lem6  19599  cyggenod  19851  gsumval3lem2  19873  gsumzadd  19889  gsum2dlem1  19937  gsum2dlem2  19938  gsum2d  19939  gsum2d2lem  19940  dprdfadd  19989  ablfac1eu  20042  pgpfac1lem5  20048  pgpfaclem2  20051  pgpfaclem3  20052  ablfaclem3  20056  prmgrpsimpgd  20083  lcomfsupp  20797  dsmmacl  21692  dsmmsubg  21694  dsmmlss  21695  frlmsslsp  21747  psrbaglecl  21876  psrbagleclOLD  21877  psrbagaddcl  21878  psrbagaddclOLD  21879  psrbagcon  21880  psrbagconOLD  21881  mplcoe5  22000  mhpmulcl  22096  psdmplcl  22109  psdmul  22113  mamures  22341  mdetrlin  22548  mdetrsca  22549  mdetralt  22554  madugsum  22589  fin1aufil  23880  xrge0gsumle  24793  xrge0tsms  24794  fsumcn  24832  rrxcph  25364  rrxmval  25377  i1fadd  25668  i1fmul  25669  i1fmulc  25677  i1fres  25679  mbfi1fseqlem4  25692  itgfsum  25800  dvmptfsum  25951  jensenlem1  26964  jensenlem2  26965  jensen  26966  0sgm  27121  sgmf  27122  sgmnncl  27124  fsumdvdsdiag  27161  fsumdvdscom  27162  dvdsflsumcom  27165  musum  27168  musumsum  27169  muinv  27170  fsumdvdsmul  27172  fsumdvdsmulOLD  27174  vmasum  27194  perfectlem2  27208  dchrfi  27233  rplogsumlem2  27463  rpvmasumlem  27465  dchrvmasumlem1  27473  dchrisum0ff  27485  dchrisum0  27498  vmalogdivsum2  27516  logsqvma  27520  logsqvma2  27521  selberg  27526  selberg34r  27549  pntsval2  27554  pntrlog2bndlem1  27555  wwlksnfi  29789  wspthnfi  29802  wspthnonfi  29805  clwwlknfi  29927  qerclwwlknfi  29955  clwlknon2num  30250  numclwlk1lem2  30252  fsuppinisegfi  32549  offinsupp1  32591  fsumiunle  32677  elrspunidl  33240  elrspunsn  33241  rprmdvdsprod  33346  fedgmullem1  33458  hashreprin  34383  reprfi2  34386  hgt750lema  34420  tgoldbachgtde  34423  aks4d1p4  41682  aks4d1p5  41683  aks4d1p7  41686  aks4d1p8  41690  evl1gprodd  41720  hashscontpowcl  41723  idomnnzgmulnz  41736  deg1gprod  41743  sticksstones3  41751  sticksstones22  41771  aks6d1c6lem5  41780  selvvvval  41953  cantnfub  42892  naddcnff  42933  finnzfsuppd  43781  fprodcnlem  45125  cnrefiisplem  45355  sge0uzfsumgt  45970  hoidmvlelem1  46121  hoidmvlelem2  46122  hoidmvlelem3  46123  hoidmvlelem4  46124  hspmbllem1  46152