Theorem ssfid 9269

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

Syntax hints:   → wi 4   ∈ wcel 2106   ⊆ wss 3948  Fincfn 8941

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7727

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-om 7858  df-1o 8468  df-en 8942  df-fin 8945

This theorem is referenced by:  ixpfi  9351  fisuppfi  9372  fsuppunbi  9386  ressuppfi  9392  fsuppmptif  9396  fsuppco2  9400  fsuppcor  9401  marypha1lem  9430  wemapso2lem  9549  cantnfp1lem1  9675  pwfseqlem4  10659  hashbclem  14415  hashf1lem2  14421  phphashd  14431  isercolllem2  15616  isercoll  15618  fsum2dlem  15720  fsumcom2  15724  fsumless  15746  fsumabs  15751  fsumrlim  15761  fsumo1  15762  fsumiun  15771  qshash  15777  incexc  15787  incexc2  15788  fprod2dlem  15928  fprodcom2  15932  4sqlem11  16892  vdwlem11  16928  ramlb  16956  0ram  16957  ramub1lem1  16963  ramub1lem2  16964  prmgaplem4  16991  isstruct2  17086  lagsubg2  19109  lagsubg  19110  orbsta2  19219  symgbasfi  19287  oddvds2  19475  sylow1lem3  19509  sylow1lem4  19510  sylow1lem5  19511  odcau  19513  pgpssslw  19523  sylow2alem2  19527  sylow2a  19528  sylow2blem1  19529  sylow2blem3  19531  slwhash  19533  fislw  19534  sylow2  19535  sylow3lem1  19536  sylow3lem3  19538  sylow3lem4  19539  sylow3lem6  19541  cyggenod  19793  gsumval3lem2  19815  gsumzadd  19831  gsum2dlem1  19879  gsum2dlem2  19880  gsum2d  19881  gsum2d2lem  19882  dprdfadd  19931  ablfac1eu  19984  pgpfac1lem5  19990  pgpfaclem2  19993  pgpfaclem3  19994  ablfaclem3  19998  prmgrpsimpgd  20025  lcomfsupp  20656  dsmmacl  21515  dsmmsubg  21517  dsmmlss  21518  frlmsslsp  21570  psrbaglecl  21698  psrbagleclOLD  21699  psrbagaddcl  21700  psrbagaddclOLD  21701  psrbagcon  21702  psrbagconOLD  21703  mplcoe5  21814  mhpmulcl  21911  mamures  22112  mdetrlin  22324  mdetrsca  22325  mdetralt  22330  madugsum  22365  fin1aufil  23656  xrge0gsumle  24569  xrge0tsms  24570  fsumcn  24608  rrxcph  25133  rrxmval  25146  i1fadd  25436  i1fmul  25437  i1fmulc  25445  i1fres  25447  mbfi1fseqlem4  25460  itgfsum  25568  dvmptfsum  25716  jensenlem1  26715  jensenlem2  26716  jensen  26717  0sgm  26872  sgmf  26873  sgmnncl  26875  fsumdvdsdiag  26912  fsumdvdscom  26913  dvdsflsumcom  26916  musum  26919  musumsum  26920  muinv  26921  fsumdvdsmul  26923  vmasum  26943  perfectlem2  26957  dchrfi  26982  rplogsumlem2  27212  rpvmasumlem  27214  dchrvmasumlem1  27222  dchrisum0ff  27234  dchrisum0  27247  vmalogdivsum2  27265  logsqvma  27269  logsqvma2  27270  selberg  27275  selberg34r  27298  pntsval2  27303  pntrlog2bndlem1  27304  wwlksnfi  29415  wspthnfi  29428  wspthnonfi  29431  clwwlknfi  29553  qerclwwlknfi  29581  clwlknon2num  29876  numclwlk1lem2  29878  fsuppinisegfi  32164  offinsupp1  32207  fsumiunle  32290  elrspunidl  32808  elrspunsn  32809  fedgmullem1  32990  hashreprin  33918  reprfi2  33921  hgt750lema  33955  tgoldbachgtde  33958  aks4d1p4  41250  aks4d1p5  41251  aks4d1p7  41254  aks4d1p8  41258  sticksstones3  41270  sticksstones22  41290  selvvvval  41459  cantnfub  42373  naddcnff  42414  finnzfsuppd  43263  fprodcnlem  44614  cnrefiisplem  44844  sge0uzfsumgt  45459  hoidmvlelem1  45610  hoidmvlelem2  45611  hoidmvlelem3  45612  hoidmvlelem4  45613  hspmbllem1  45641