Theorem ssfid 9260

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ⊆ wss 3895  Fincfn 8973

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-om 7878  df-1o 8476  df-en 8974  df-fin 8977

This theorem is used by:  ixpfi  9338  fisuppfi  9363  finnzfsuppd  9365  fsuppunbi  9381  ressuppfi  9387  fsuppmptif  9391  fsuppco2  9395  fsuppcor  9396  marypha1lem  9425  wemapso2lem  9546  cantnfp1lem1  9679  pwfseqlem4  10747  hashpss  14554  hashbclem  14597  hashf1lem2  14601  phphashd  14611  isercolllem2  15833  isercoll  15835  fsum2dlem  15936  fsumcom2  15940  fsumless  15963  fsumabs  15968  fsumrlim  15978  fsumo1  15979  fsumiun  15988  qshash  15994  incexc  16006  incexc2  16007  fprod2dlem  16147  fprodcom2  16151  dvdsfi  16966  4sqlem11  17133  vdwlem11  17169  ramlb  17197  0ram  17198  ramub1lem1  17204  ramub1lem2  17205  prmgaplem4  17232  isstruct2  17327  lagsubg2  19409  lagsubg  19410  orbsta2  19528  symgbasfi  19593  oddvds2  19780  sylow1lem3  19814  sylow1lem4  19815  sylow1lem5  19816  odcau  19818  pgpssslw  19828  sylow2alem2  19832  sylow2a  19833  sylow2blem1  19834  sylow2blem3  19836  slwhash  19838  fislw  19839  sylow2  19840  sylow3lem1  19841  sylow3lem3  19843  sylow3lem4  19844  sylow3lem6  19846  cyggenod  20098  gsumval3lem2  20120  gsumzadd  20136  gsum2dlem1  20184  gsum2dlem2  20185  gsum2d  20186  gsum2d2lem  20187  dprdfadd  20236  ablfac1eu  20289  pgpfac1lem5  20295  pgpfaclem2  20298  pgpfaclem3  20299  ablfaclem3  20303  prmgrpsimpgd  20330  lcomfsupp  21177  dsmmacl  22047  dsmmsubg  22049  dsmmlss  22050  frlmsslsp  22102  psrbaglecl  22231  psrbagaddcl  22232  psrbagcon  22233  mplcoe5  22349  selvvvval  22451  mhpmulcl  22470  psdmplcl  22483  psdmul  22487  mamures  22712  mdetrlin  22917  mdetrsca  22918  mdetralt  22923  madugsum  22958  fin1aufil  24251  xrge0gsumle  25153  xrge0tsms  25154  fsumcn  25191  rrxcph  25713  rrxmval  25726  i1fadd  26016  i1fmul  26017  i1fmulc  26024  i1fres  26026  mbfi1fseqlem4  26039  itgfsum  26147  dvmptfsum  26295  plyconz  26631  jensenlem1  27314  jensenlem2  27315  jensen  27316  sgmf  27472  sgmnncl  27474  fsumdvdsdiag  27511  fsumdvdscom  27512  dvdsflsumcom  27515  musum  27518  musumsum  27519  muinv  27520  fsumdvdsmul  27522  perfectlem2  27557  dchrfi  27582  rplogsumlem2  27812  rpvmasumlem  27814  dchrvmasumlem1  27822  dchrisum0ff  27834  dchrisum0  27847  vmalogdivsum2  27865  logsqvma  27869  selberg  27875  selberg34r  27898  pntsval2  27903  pntrlog2bndlem1  27904  onsfi  28742  wwlksnfi  30495  wspthnfi  30508  wspthnonfi  30511  clwwlknfi  30636  qerclwwlknfi  30664  clwlknon2num  30969  numclwlk1lem2  30971  fsuppinisegfi  33322  offinsupp1  33360  fsumiunle  33462  elrgspnlem2  33846  elrgspnlem4  33848  elrgspnsubrunlem2  33851  domnprodeq0  33882  elrspunidl  34020  elrspunsn  34021  rprmdvdsprod  34108  deg1prod  34157  mplidomlem  34201  psrgsum  34222  psrmonprod  34226  esplyfval2  34239  esplymhp  34242  esplyind  34249  esplyindfv  34250  esplyfvn  34251  vieta  34254  exsslsb  34271  fedgmullem1  34303  fldextrspunlsplem  34347  constrfin  34420  hashreprin  35291  reprfi2  35294  hgt750lema  35328  tgoldbachgtde  35331  kardnnfi  35879  aks4d1p4  43172  aks4d1p5  43173  aks4d1p7  43176  aks4d1p8  43180  evl1gprodd  43210  hashscontpowcl  43213  idomnnzgmulnz  43226  deg1gprod  43233  sticksstones3  43241  sticksstones22  43261  aks6d1c6lem5  43270  grpods  43287  unitscyglem1  43288  unitscyglem2  43289  unitscyglem4  43291  unitscyglem5  43292  frlmnzcoordcl  43698  frlmnzcoordn0  43700  cantnfub  44366  naddcnff  44407  fprodcnlem  46654  sumnnodd  46685  cnrefiisplem  46882  dvmptfprod  46998  dvnprodlem1  46999  sge0uzfsumgt  47497  hoidmvlelem1  47648  hoidmvlelem2  47649  hoidmvlelem3  47650  hoidmvlelem4  47651  hspmbllem1  47679