Theorem ssfid 9170

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3905  Fincfn 8879

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7675

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-om 7807  df-1o 8395  df-en 8880  df-fin 8883

This theorem is referenced by:  ixpfi  9258  fisuppfi  9280  finnzfsuppd  9282  fsuppunbi  9298  ressuppfi  9304  fsuppmptif  9308  fsuppco2  9312  fsuppcor  9313  marypha1lem  9342  wemapso2lem  9463  cantnfp1lem1  9593  pwfseqlem4  10575  hashbclem  14377  hashf1lem2  14381  phphashd  14391  isercolllem2  15591  isercoll  15593  fsum2dlem  15695  fsumcom2  15699  fsumless  15721  fsumabs  15726  fsumrlim  15736  fsumo1  15737  fsumiun  15746  qshash  15752  incexc  15762  incexc2  15763  fprod2dlem  15905  fprodcom2  15909  dvdsfi  16718  4sqlem11  16885  vdwlem11  16921  ramlb  16949  0ram  16950  ramub1lem1  16956  ramub1lem2  16957  prmgaplem4  16984  isstruct2  17078  lagsubg2  19091  lagsubg  19092  orbsta2  19211  symgbasfi  19276  oddvds2  19463  sylow1lem3  19497  sylow1lem4  19498  sylow1lem5  19499  odcau  19501  pgpssslw  19511  sylow2alem2  19515  sylow2a  19516  sylow2blem1  19517  sylow2blem3  19519  slwhash  19521  fislw  19522  sylow2  19523  sylow3lem1  19524  sylow3lem3  19526  sylow3lem4  19527  sylow3lem6  19529  cyggenod  19781  gsumval3lem2  19803  gsumzadd  19819  gsum2dlem1  19867  gsum2dlem2  19868  gsum2d  19869  gsum2d2lem  19870  dprdfadd  19919  ablfac1eu  19972  pgpfac1lem5  19978  pgpfaclem2  19981  pgpfaclem3  19982  ablfaclem3  19986  prmgrpsimpgd  20013  lcomfsupp  20823  dsmmacl  21666  dsmmsubg  21668  dsmmlss  21669  frlmsslsp  21721  psrbaglecl  21848  psrbagaddcl  21849  psrbagcon  21850  mplcoe5  21963  mhpmulcl  22052  psdmplcl  22065  psdmul  22069  mamures  22300  mdetrlin  22505  mdetrsca  22506  mdetralt  22511  madugsum  22546  fin1aufil  23835  xrge0gsumle  24738  xrge0tsms  24739  fsumcn  24777  rrxcph  25308  rrxmval  25321  i1fadd  25612  i1fmul  25613  i1fmulc  25620  i1fres  25622  mbfi1fseqlem4  25635  itgfsum  25744  dvmptfsum  25895  jensenlem1  26913  jensenlem2  26914  jensen  26915  sgmf  27071  sgmnncl  27073  fsumdvdsdiag  27110  fsumdvdscom  27111  dvdsflsumcom  27114  musum  27117  musumsum  27118  muinv  27119  fsumdvdsmul  27121  fsumdvdsmulOLD  27123  perfectlem2  27157  dchrfi  27182  rplogsumlem2  27412  rpvmasumlem  27414  dchrvmasumlem1  27422  dchrisum0ff  27434  dchrisum0  27447  vmalogdivsum2  27465  logsqvma  27469  selberg  27475  selberg34r  27498  pntsval2  27503  pntrlog2bndlem1  27504  onsfi  28270  wwlksnfi  29869  wspthnfi  29882  wspthnonfi  29885  clwwlknfi  30007  qerclwwlknfi  30035  clwlknon2num  30330  numclwlk1lem2  30332  fsuppinisegfi  32643  offinsupp1  32683  hashpss  32767  fsumiunle  32787  elrgspnlem2  33193  elrgspnlem4  33195  elrgspnsubrunlem2  33198  elrspunidl  33375  elrspunsn  33376  rprmdvdsprod  33481  exsslsb  33568  fedgmullem1  33601  fldextrspunlsplem  33644  constrfin  33712  hashreprin  34587  reprfi2  34590  hgt750lema  34624  tgoldbachgtde  34627  aks4d1p4  42052  aks4d1p5  42053  aks4d1p7  42056  aks4d1p8  42060  evl1gprodd  42090  hashscontpowcl  42093  idomnnzgmulnz  42106  deg1gprod  42113  sticksstones3  42121  sticksstones22  42141  aks6d1c6lem5  42150  grpods  42167  unitscyglem1  42168  unitscyglem2  42169  unitscyglem4  42171  unitscyglem5  42172  selvvvval  42558  cantnfub  43294  naddcnff  43335  fprodcnlem  45581  cnrefiisplem  45811  dvmptfprod  45927  dvnprodlem1  45928  sge0uzfsumgt  46426  hoidmvlelem1  46577  hoidmvlelem2  46578  hoidmvlelem3  46579  hoidmvlelem4  46580  hspmbllem1  46608