Theorem ssfid 9174

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3902  Fincfn 8888

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 5242  ax-nul 5252  ax-pr 5378  ax-un 7683

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 3062  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-tr 5207  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-om 7812  df-1o 8400  df-en 8889  df-fin 8892

This theorem is referenced by:  ixpfi  9254  fisuppfi  9279  finnzfsuppd  9281  fsuppunbi  9297  ressuppfi  9303  fsuppmptif  9307  fsuppco2  9311  fsuppcor  9312  marypha1lem  9341  wemapso2lem  9462  cantnfp1lem1  9592  pwfseqlem4  10578  hashbclem  14380  hashf1lem2  14384  phphashd  14394  isercolllem2  15594  isercoll  15596  fsum2dlem  15698  fsumcom2  15702  fsumless  15724  fsumabs  15729  fsumrlim  15739  fsumo1  15740  fsumiun  15749  qshash  15755  incexc  15765  incexc2  15766  fprod2dlem  15908  fprodcom2  15912  dvdsfi  16721  4sqlem11  16888  vdwlem11  16924  ramlb  16952  0ram  16953  ramub1lem1  16959  ramub1lem2  16960  prmgaplem4  16987  isstruct2  17081  lagsubg2  19128  lagsubg  19129  orbsta2  19248  symgbasfi  19313  oddvds2  19500  sylow1lem3  19534  sylow1lem4  19535  sylow1lem5  19536  odcau  19538  pgpssslw  19548  sylow2alem2  19552  sylow2a  19553  sylow2blem1  19554  sylow2blem3  19556  slwhash  19558  fislw  19559  sylow2  19560  sylow3lem1  19561  sylow3lem3  19563  sylow3lem4  19564  sylow3lem6  19566  cyggenod  19818  gsumval3lem2  19840  gsumzadd  19856  gsum2dlem1  19904  gsum2dlem2  19905  gsum2d  19906  gsum2d2lem  19907  dprdfadd  19956  ablfac1eu  20009  pgpfac1lem5  20015  pgpfaclem2  20018  pgpfaclem3  20019  ablfaclem3  20023  prmgrpsimpgd  20050  lcomfsupp  20858  dsmmacl  21701  dsmmsubg  21703  dsmmlss  21704  frlmsslsp  21756  psrbaglecl  21884  psrbagaddcl  21885  psrbagcon  21886  mplcoe5  22000  mhpmulcl  22097  psdmplcl  22110  psdmul  22114  mamures  22346  mdetrlin  22551  mdetrsca  22552  mdetralt  22557  madugsum  22592  fin1aufil  23881  xrge0gsumle  24783  xrge0tsms  24784  fsumcn  24822  rrxcph  25353  rrxmval  25366  i1fadd  25657  i1fmul  25658  i1fmulc  25665  i1fres  25667  mbfi1fseqlem4  25680  itgfsum  25789  dvmptfsum  25940  jensenlem1  26958  jensenlem2  26959  jensen  26960  sgmf  27116  sgmnncl  27118  fsumdvdsdiag  27155  fsumdvdscom  27156  dvdsflsumcom  27159  musum  27162  musumsum  27163  muinv  27164  fsumdvdsmul  27166  fsumdvdsmulOLD  27168  perfectlem2  27202  dchrfi  27227  rplogsumlem2  27457  rpvmasumlem  27459  dchrvmasumlem1  27467  dchrisum0ff  27479  dchrisum0  27492  vmalogdivsum2  27510  logsqvma  27514  selberg  27520  selberg34r  27543  pntsval2  27548  pntrlog2bndlem1  27549  onsfi  28357  wwlksnfi  29984  wspthnfi  29997  wspthnonfi  30000  clwwlknfi  30125  qerclwwlknfi  30153  clwlknon2num  30448  numclwlk1lem2  30450  fsuppinisegfi  32769  offinsupp1  32808  hashpss  32892  fsumiunle  32913  elrgspnlem2  33329  elrgspnlem4  33331  elrgspnsubrunlem2  33334  domnprodeq0  33362  elrspunidl  33513  elrspunsn  33514  rprmdvdsprod  33619  deg1prod  33668  psrgsum  33717  psrmonprod  33721  esplyfval2  33734  esplymhp  33737  esplyind  33744  esplyindfv  33745  esplyfvn  33746  vieta  33749  exsslsb  33766  fedgmullem1  33799  fldextrspunlsplem  33843  constrfin  33916  hashreprin  34790  reprfi2  34793  hgt750lema  34827  tgoldbachgtde  34830  aks4d1p4  42412  aks4d1p5  42413  aks4d1p7  42416  aks4d1p8  42420  evl1gprodd  42450  hashscontpowcl  42453  idomnnzgmulnz  42466  deg1gprod  42473  sticksstones3  42481  sticksstones22  42501  aks6d1c6lem5  42510  grpods  42527  unitscyglem1  42528  unitscyglem2  42529  unitscyglem4  42531  unitscyglem5  42532  selvvvval  42906  cantnfub  43641  naddcnff  43682  fprodcnlem  45922  cnrefiisplem  46150  dvmptfprod  46266  dvnprodlem1  46267  sge0uzfsumgt  46765  hoidmvlelem1  46916  hoidmvlelem2  46917  hoidmvlelem3  46918  hoidmvlelem4  46919  hspmbllem1  46947