Theorem ssfid 9086

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

Syntax hints:   → wi 4   ∈ wcel 2104   ⊆ wss 3892  Fincfn 8764

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361  ax-un 7620

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-opab 5144  df-tr 5199  df-id 5500  df-eprel 5506  df-po 5514  df-so 5515  df-fr 5555  df-we 5557  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-ord 6284  df-on 6285  df-lim 6286  df-suc 6287  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-om 7745  df-1o 8328  df-en 8765  df-fin 8768

This theorem is referenced by:  ixpfi  9160  fisuppfi  9180  fsuppunbi  9193  ressuppfi  9198  fsuppmptif  9202  fsuppco2  9206  fsuppcor  9207  marypha1lem  9236  wemapso2lem  9355  cantnfp1lem1  9480  pwfseqlem4  10464  hashbclem  14209  hashf1lem2  14215  phphashd  14225  isercolllem2  15422  isercoll  15424  fsum2dlem  15527  fsumcom2  15531  fsumless  15553  fsumabs  15558  fsumrlim  15568  fsumo1  15569  fsumiun  15578  qshash  15584  incexc  15594  incexc2  15595  fprod2dlem  15735  fprodcom2  15739  4sqlem11  16701  vdwlem11  16737  ramlb  16765  0ram  16766  ramub1lem1  16772  ramub1lem2  16773  prmgaplem4  16800  isstruct2  16895  lagsubg2  18862  lagsubg  18863  orbsta2  18965  symgbasfi  19031  oddvds2  19218  sylow1lem3  19250  sylow1lem4  19251  sylow1lem5  19252  odcau  19254  pgpssslw  19264  sylow2alem2  19268  sylow2a  19269  sylow2blem1  19270  sylow2blem3  19272  slwhash  19274  fislw  19275  sylow2  19276  sylow3lem1  19277  sylow3lem3  19279  sylow3lem4  19280  sylow3lem6  19282  cyggenod  19529  gsumval3lem2  19552  gsumzadd  19568  gsum2dlem1  19616  gsum2dlem2  19617  gsum2d  19618  gsum2d2lem  19619  dprdfadd  19668  ablfac1eu  19721  pgpfac1lem5  19727  pgpfaclem2  19730  pgpfaclem3  19731  ablfaclem3  19735  prmgrpsimpgd  19762  lcomfsupp  20208  dsmmacl  20993  dsmmsubg  20995  dsmmlss  20996  frlmsslsp  21048  psrbaglecl  21174  psrbagleclOLD  21175  psrbagaddcl  21176  psrbagaddclOLD  21177  psrbagcon  21178  psrbagconOLD  21179  mplcoe5  21286  mhpmulcl  21384  mamures  21584  mdetrlin  21796  mdetrsca  21797  mdetralt  21802  madugsum  21837  fin1aufil  23128  xrge0gsumle  24041  xrge0tsms  24042  fsumcn  24078  rrxcph  24601  rrxmval  24614  i1fadd  24904  i1fmul  24905  i1fmulc  24913  i1fres  24915  mbfi1fseqlem4  24928  itgfsum  25036  dvmptfsum  25184  jensenlem1  26181  jensenlem2  26182  jensen  26183  0sgm  26338  sgmf  26339  sgmnncl  26341  fsumdvdsdiag  26378  fsumdvdscom  26379  dvdsflsumcom  26382  musum  26385  musumsum  26386  muinv  26387  fsumdvdsmul  26389  vmasum  26409  perfectlem2  26423  dchrfi  26448  rplogsumlem2  26678  rpvmasumlem  26680  dchrvmasumlem1  26688  dchrisum0ff  26700  dchrisum0  26713  vmalogdivsum2  26731  logsqvma  26735  logsqvma2  26736  selberg  26741  selberg34r  26764  pntsval2  26769  pntrlog2bndlem1  26770  wwlksnfi  28316  wspthnfi  28329  wspthnonfi  28332  clwwlknfi  28454  qerclwwlknfi  28482  clwlknon2num  28777  numclwlk1lem2  28779  fsuppinisegfi  31066  offinsupp1  31107  fsumiunle  31188  elrspunidl  31651  fedgmullem1  31755  hashreprin  32645  reprfi2  32648  hgt750lema  32682  tgoldbachgtde  32685  aks4d1p4  40129  aks4d1p5  40130  aks4d1p7  40133  aks4d1p8  40137  sticksstones3  40146  sticksstones22  40166  evlsbagval  40312  mhphf  40322  finnzfsuppd  41858  fprodcnlem  43189  cnrefiisplem  43419  sge0uzfsumgt  44032  hoidmvlelem1  44183  hoidmvlelem2  44184  hoidmvlelem3  44185  hoidmvlelem4  44186  hspmbllem1  44214