Theorem ssfid 9148

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

Syntax hints:   → wi 4   ∈ wcel 2110   ⊆ wss 3900  Fincfn 8864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-un 7663

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3345  df-rab 3394  df-v 3436  df-sbc 3740  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-pss 3920  df-nul 4282  df-if 4474  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-opab 5152  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6433  df-fun 6479  df-fn 6480  df-f 6481  df-f1 6482  df-fo 6483  df-f1o 6484  df-fv 6485  df-om 7792  df-1o 8380  df-en 8865  df-fin 8868

This theorem is referenced by:  ixpfi  9228  fisuppfi  9250  finnzfsuppd  9252  fsuppunbi  9268  ressuppfi  9274  fsuppmptif  9278  fsuppco2  9282  fsuppcor  9283  marypha1lem  9312  wemapso2lem  9433  cantnfp1lem1  9563  pwfseqlem4  10545  hashbclem  14351  hashf1lem2  14355  phphashd  14365  isercolllem2  15565  isercoll  15567  fsum2dlem  15669  fsumcom2  15673  fsumless  15695  fsumabs  15700  fsumrlim  15710  fsumo1  15711  fsumiun  15720  qshash  15726  incexc  15736  incexc2  15737  fprod2dlem  15879  fprodcom2  15883  dvdsfi  16692  4sqlem11  16859  vdwlem11  16895  ramlb  16923  0ram  16924  ramub1lem1  16930  ramub1lem2  16931  prmgaplem4  16958  isstruct2  17052  lagsubg2  19099  lagsubg  19100  orbsta2  19219  symgbasfi  19284  oddvds2  19471  sylow1lem3  19505  sylow1lem4  19506  sylow1lem5  19507  odcau  19509  pgpssslw  19519  sylow2alem2  19523  sylow2a  19524  sylow2blem1  19525  sylow2blem3  19527  slwhash  19529  fislw  19530  sylow2  19531  sylow3lem1  19532  sylow3lem3  19534  sylow3lem4  19535  sylow3lem6  19537  cyggenod  19789  gsumval3lem2  19811  gsumzadd  19827  gsum2dlem1  19875  gsum2dlem2  19876  gsum2d  19877  gsum2d2lem  19878  dprdfadd  19927  ablfac1eu  19980  pgpfac1lem5  19986  pgpfaclem2  19989  pgpfaclem3  19990  ablfaclem3  19994  prmgrpsimpgd  20021  lcomfsupp  20828  dsmmacl  21671  dsmmsubg  21673  dsmmlss  21674  frlmsslsp  21726  psrbaglecl  21853  psrbagaddcl  21854  psrbagcon  21855  mplcoe5  21968  mhpmulcl  22057  psdmplcl  22070  psdmul  22074  mamures  22305  mdetrlin  22510  mdetrsca  22511  mdetralt  22516  madugsum  22551  fin1aufil  23840  xrge0gsumle  24742  xrge0tsms  24743  fsumcn  24781  rrxcph  25312  rrxmval  25325  i1fadd  25616  i1fmul  25617  i1fmulc  25624  i1fres  25626  mbfi1fseqlem4  25639  itgfsum  25748  dvmptfsum  25899  jensenlem1  26917  jensenlem2  26918  jensen  26919  sgmf  27075  sgmnncl  27077  fsumdvdsdiag  27114  fsumdvdscom  27115  dvdsflsumcom  27118  musum  27121  musumsum  27122  muinv  27123  fsumdvdsmul  27125  fsumdvdsmulOLD  27127  perfectlem2  27161  dchrfi  27186  rplogsumlem2  27416  rpvmasumlem  27418  dchrvmasumlem1  27426  dchrisum0ff  27438  dchrisum0  27451  vmalogdivsum2  27469  logsqvma  27473  selberg  27479  selberg34r  27502  pntsval2  27507  pntrlog2bndlem1  27508  onsfi  28276  wwlksnfi  29877  wspthnfi  29890  wspthnonfi  29893  clwwlknfi  30015  qerclwwlknfi  30043  clwlknon2num  30338  numclwlk1lem2  30340  fsuppinisegfi  32658  offinsupp1  32699  hashpss  32781  fsumiunle  32802  elrgspnlem2  33200  elrgspnlem4  33202  elrgspnsubrunlem2  33205  elrspunidl  33383  elrspunsn  33384  rprmdvdsprod  33489  esplymhp  33579  exsslsb  33599  fedgmullem1  33632  fldextrspunlsplem  33676  constrfin  33749  hashreprin  34623  reprfi2  34626  hgt750lema  34660  tgoldbachgtde  34663  aks4d1p4  42091  aks4d1p5  42092  aks4d1p7  42095  aks4d1p8  42099  evl1gprodd  42129  hashscontpowcl  42132  idomnnzgmulnz  42145  deg1gprod  42152  sticksstones3  42160  sticksstones22  42180  aks6d1c6lem5  42189  grpods  42206  unitscyglem1  42207  unitscyglem2  42208  unitscyglem4  42210  unitscyglem5  42211  selvvvval  42597  cantnfub  43333  naddcnff  43374  fprodcnlem  45618  cnrefiisplem  45846  dvmptfprod  45962  dvnprodlem1  45963  sge0uzfsumgt  46461  hoidmvlelem1  46612  hoidmvlelem2  46613  hoidmvlelem3  46614  hoidmvlelem4  46615  hspmbllem1  46643