Theorem ssfid 9213

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

Syntax hints:   → wi 4   ∈ wcel 2143   ⊆ wss 3905  Fincfn 8927

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pr 5391  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3078  df-rex 3088  df-reu 3369  df-rab 3416  df-v 3457  df-sbc 3746  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-opab 5164  df-tr 5209  df-id 5543  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-we 5603  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-om 7847  df-1o 8437  df-en 8928  df-fin 8931

This theorem is referenced by:  ixpfi  9290  fisuppfi  9315  finnzfsuppd  9317  fsuppunbi  9333  ressuppfi  9339  fsuppmptif  9343  fsuppco2  9347  fsuppcor  9348  marypha1lem  9377  wemapso2lem  9498  cantnfp1lem1  9631  pwfseqlem4  10631  hashbclem  14475  hashf1lem2  14479  phphashd  14489  isercolllem2  15703  isercoll  15705  fsum2dlem  15807  fsumcom2  15811  fsumless  15834  fsumabs  15839  fsumrlim  15849  fsumo1  15850  fsumiun  15859  qshash  15865  incexc  15877  incexc2  15878  fprod2dlem  16020  fprodcom2  16024  dvdsfi  16834  4sqlem11  17001  vdwlem11  17037  ramlb  17065  0ram  17066  ramub1lem1  17072  ramub1lem2  17073  prmgaplem4  17100  isstruct2  17195  lagsubg2  19245  lagsubg  19246  orbsta2  19364  symgbasfi  19429  oddvds2  19616  sylow1lem3  19650  sylow1lem4  19651  sylow1lem5  19652  odcau  19654  pgpssslw  19664  sylow2alem2  19668  sylow2a  19669  sylow2blem1  19670  sylow2blem3  19672  slwhash  19674  fislw  19675  sylow2  19676  sylow3lem1  19677  sylow3lem3  19679  sylow3lem4  19680  sylow3lem6  19682  cyggenod  19934  gsumval3lem2  19956  gsumzadd  19972  gsum2dlem1  20020  gsum2dlem2  20021  gsum2d  20022  gsum2d2lem  20023  dprdfadd  20072  ablfac1eu  20125  pgpfac1lem5  20131  pgpfaclem2  20134  pgpfaclem3  20135  ablfaclem3  20139  prmgrpsimpgd  20166  lcomfsupp  20976  dsmmacl  21800  dsmmsubg  21802  dsmmlss  21803  frlmsslsp  21855  psrbaglecl  21982  psrbagaddcl  21983  psrbagcon  21984  mplcoe5  22100  selvvvval  22202  mhpmulcl  22221  psdmplcl  22234  psdmul  22238  mamures  22464  mdetrlin  22669  mdetrsca  22670  mdetralt  22675  madugsum  22710  fin1aufil  23999  xrge0gsumle  24901  xrge0tsms  24902  fsumcn  24939  rrxcph  25461  rrxmval  25474  i1fadd  25764  i1fmul  25765  i1fmulc  25772  i1fres  25774  mbfi1fseqlem4  25787  itgfsum  25896  dvmptfsum  26044  jensenlem1  27058  jensenlem2  27059  jensen  27060  sgmf  27216  sgmnncl  27218  fsumdvdsdiag  27255  fsumdvdscom  27256  dvdsflsumcom  27259  musum  27262  musumsum  27263  muinv  27264  fsumdvdsmul  27266  perfectlem2  27301  dchrfi  27326  rplogsumlem2  27556  rpvmasumlem  27558  dchrvmasumlem1  27566  dchrisum0ff  27578  dchrisum0  27591  vmalogdivsum2  27609  logsqvma  27613  selberg  27619  selberg34r  27642  pntsval2  27647  pntrlog2bndlem1  27648  onsfi  28456  wwlksnfi  30113  wspthnfi  30126  wspthnonfi  30129  clwwlknfi  30254  qerclwwlknfi  30282  clwlknon2num  30577  numclwlk1lem2  30579  fsuppinisegfi  32895  offinsupp1  32934  hashpss  33017  fsumiunle  33037  elrgspnlem2  33430  elrgspnlem4  33432  elrgspnsubrunlem2  33435  domnprodeq0  33466  elrspunidl  33617  elrspunsn  33618  rprmdvdsprod  33733  deg1prod  33782  mplidomlem  33826  psrgsum  33847  psrmonprod  33851  esplyfval2  33864  esplymhp  33867  esplyind  33874  esplyindfv  33875  esplyfvn  33876  vieta  33879  exsslsb  33896  fedgmullem1  33928  fldextrspunlsplem  33972  constrfin  34045  hashreprin  34916  reprfi2  34919  hgt750lema  34953  tgoldbachgtde  34956  aks4d1p4  42701  aks4d1p5  42702  aks4d1p7  42705  aks4d1p8  42709  evl1gprodd  42739  hashscontpowcl  42742  idomnnzgmulnz  42755  deg1gprod  42762  sticksstones3  42770  sticksstones22  42790  aks6d1c6lem5  42799  grpods  42816  unitscyglem1  42817  unitscyglem2  42818  unitscyglem4  42820  unitscyglem5  42821  cantnfub  43903  naddcnff  43944  fprodcnlem  46166  cnrefiisplem  46394  dvmptfprod  46510  dvnprodlem1  46511  sge0uzfsumgt  47009  hoidmvlelem1  47160  hoidmvlelem2  47161  hoidmvlelem3  47162  hoidmvlelem4  47163  hspmbllem1  47191