Theorem ssfid 9179

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3890  Fincfn 8893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5376  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-tr 5194  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-ord 6327  df-on 6328  df-lim 6329  df-suc 6330  df-iota 6455  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-om 7818  df-1o 8405  df-en 8894  df-fin 8897

This theorem is referenced by:  ixpfi  9259  fisuppfi  9284  finnzfsuppd  9286  fsuppunbi  9302  ressuppfi  9308  fsuppmptif  9312  fsuppco2  9316  fsuppcor  9317  marypha1lem  9346  wemapso2lem  9467  cantnfp1lem1  9599  pwfseqlem4  10585  hashbclem  14414  hashf1lem2  14418  phphashd  14428  isercolllem2  15628  isercoll  15630  fsum2dlem  15732  fsumcom2  15736  fsumless  15759  fsumabs  15764  fsumrlim  15774  fsumo1  15775  fsumiun  15784  qshash  15790  incexc  15802  incexc2  15803  fprod2dlem  15945  fprodcom2  15949  dvdsfi  16759  4sqlem11  16926  vdwlem11  16962  ramlb  16990  0ram  16991  ramub1lem1  16997  ramub1lem2  16998  prmgaplem4  17025  isstruct2  17119  lagsubg2  19169  lagsubg  19170  orbsta2  19289  symgbasfi  19354  oddvds2  19541  sylow1lem3  19575  sylow1lem4  19576  sylow1lem5  19577  odcau  19579  pgpssslw  19589  sylow2alem2  19593  sylow2a  19594  sylow2blem1  19595  sylow2blem3  19597  slwhash  19599  fislw  19600  sylow2  19601  sylow3lem1  19602  sylow3lem3  19604  sylow3lem4  19605  sylow3lem6  19607  cyggenod  19859  gsumval3lem2  19881  gsumzadd  19897  gsum2dlem1  19945  gsum2dlem2  19946  gsum2d  19947  gsum2d2lem  19948  dprdfadd  19997  ablfac1eu  20050  pgpfac1lem5  20056  pgpfaclem2  20059  pgpfaclem3  20060  ablfaclem3  20064  prmgrpsimpgd  20091  lcomfsupp  20897  dsmmacl  21721  dsmmsubg  21723  dsmmlss  21724  frlmsslsp  21776  psrbaglecl  21903  psrbagaddcl  21904  psrbagcon  21905  mplcoe5  22018  mhpmulcl  22115  psdmplcl  22128  psdmul  22132  mamures  22362  mdetrlin  22567  mdetrsca  22568  mdetralt  22573  madugsum  22608  fin1aufil  23897  xrge0gsumle  24799  xrge0tsms  24800  fsumcn  24837  rrxcph  25359  rrxmval  25372  i1fadd  25662  i1fmul  25663  i1fmulc  25670  i1fres  25672  mbfi1fseqlem4  25685  itgfsum  25794  dvmptfsum  25942  jensenlem1  26950  jensenlem2  26951  jensen  26952  sgmf  27108  sgmnncl  27110  fsumdvdsdiag  27147  fsumdvdscom  27148  dvdsflsumcom  27151  musum  27154  musumsum  27155  muinv  27156  fsumdvdsmul  27158  perfectlem2  27193  dchrfi  27218  rplogsumlem2  27448  rpvmasumlem  27450  dchrvmasumlem1  27458  dchrisum0ff  27470  dchrisum0  27483  vmalogdivsum2  27501  logsqvma  27505  selberg  27511  selberg34r  27534  pntsval2  27539  pntrlog2bndlem1  27540  onsfi  28348  wwlksnfi  29974  wspthnfi  29987  wspthnonfi  29990  clwwlknfi  30115  qerclwwlknfi  30143  clwlknon2num  30438  numclwlk1lem2  30440  fsuppinisegfi  32760  offinsupp1  32799  hashpss  32882  fsumiunle  32902  elrgspnlem2  33304  elrgspnlem4  33306  elrgspnsubrunlem2  33309  domnprodeq0  33337  elrspunidl  33488  elrspunsn  33489  rprmdvdsprod  33594  deg1prod  33643  psrgsum  33692  psrmonprod  33696  esplyfval2  33709  esplymhp  33712  esplyind  33719  esplyindfv  33720  esplyfvn  33721  vieta  33724  exsslsb  33741  fedgmullem1  33773  fldextrspunlsplem  33817  constrfin  33890  hashreprin  34764  reprfi2  34767  hgt750lema  34801  tgoldbachgtde  34804  aks4d1p4  42518  aks4d1p5  42519  aks4d1p7  42522  aks4d1p8  42526  evl1gprodd  42556  hashscontpowcl  42559  idomnnzgmulnz  42572  deg1gprod  42579  sticksstones3  42587  sticksstones22  42607  aks6d1c6lem5  42616  grpods  42633  unitscyglem1  42634  unitscyglem2  42635  unitscyglem4  42637  unitscyglem5  42638  selvvvval  43018  cantnfub  43749  naddcnff  43790  fprodcnlem  46029  cnrefiisplem  46257  dvmptfprod  46373  dvnprodlem1  46374  sge0uzfsumgt  46872  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvlelem4  47026  hspmbllem1  47054