Theorem ssfid 9298

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

Syntax hints:   → wi 4   ∈ wcel 2105   ⊆ wss 3962  Fincfn 8983

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-om 7887  df-1o 8504  df-en 8984  df-fin 8987

This theorem is referenced by:  ixpfi  9386  fisuppfi  9408  finnzfsuppd  9410  fsuppunbi  9426  ressuppfi  9432  fsuppmptif  9436  fsuppco2  9440  fsuppcor  9441  marypha1lem  9470  wemapso2lem  9589  cantnfp1lem1  9715  pwfseqlem4  10699  hashbclem  14487  hashf1lem2  14491  phphashd  14501  isercolllem2  15698  isercoll  15700  fsum2dlem  15802  fsumcom2  15806  fsumless  15828  fsumabs  15833  fsumrlim  15843  fsumo1  15844  fsumiun  15853  qshash  15859  incexc  15869  incexc2  15870  fprod2dlem  16012  fprodcom2  16016  4sqlem11  16988  vdwlem11  17024  ramlb  17052  0ram  17053  ramub1lem1  17059  ramub1lem2  17060  prmgaplem4  17087  isstruct2  17182  lagsubg2  19224  lagsubg  19225  orbsta2  19344  symgbasfi  19410  oddvds2  19598  sylow1lem3  19632  sylow1lem4  19633  sylow1lem5  19634  odcau  19636  pgpssslw  19646  sylow2alem2  19650  sylow2a  19651  sylow2blem1  19652  sylow2blem3  19654  slwhash  19656  fislw  19657  sylow2  19658  sylow3lem1  19659  sylow3lem3  19661  sylow3lem4  19662  sylow3lem6  19664  cyggenod  19916  gsumval3lem2  19938  gsumzadd  19954  gsum2dlem1  20002  gsum2dlem2  20003  gsum2d  20004  gsum2d2lem  20005  dprdfadd  20054  ablfac1eu  20107  pgpfac1lem5  20113  pgpfaclem2  20116  pgpfaclem3  20117  ablfaclem3  20121  prmgrpsimpgd  20148  lcomfsupp  20916  dsmmacl  21778  dsmmsubg  21780  dsmmlss  21781  frlmsslsp  21833  psrbaglecl  21960  psrbagaddcl  21961  psrbagcon  21962  mplcoe5  22075  mhpmulcl  22170  psdmplcl  22183  psdmul  22187  mamures  22416  mdetrlin  22623  mdetrsca  22624  mdetralt  22629  madugsum  22664  fin1aufil  23955  xrge0gsumle  24868  xrge0tsms  24869  fsumcn  24907  rrxcph  25439  rrxmval  25452  i1fadd  25743  i1fmul  25744  i1fmulc  25752  i1fres  25754  mbfi1fseqlem4  25767  itgfsum  25876  dvmptfsum  26027  jensenlem1  27044  jensenlem2  27045  jensen  27046  0sgm  27201  sgmf  27202  sgmnncl  27204  fsumdvdsdiag  27241  fsumdvdscom  27242  dvdsflsumcom  27245  musum  27248  musumsum  27249  muinv  27250  fsumdvdsmul  27252  fsumdvdsmulOLD  27254  vmasum  27274  perfectlem2  27288  dchrfi  27313  rplogsumlem2  27543  rpvmasumlem  27545  dchrvmasumlem1  27553  dchrisum0ff  27565  dchrisum0  27578  vmalogdivsum2  27596  logsqvma  27600  logsqvma2  27601  selberg  27606  selberg34r  27629  pntsval2  27634  pntrlog2bndlem1  27635  wwlksnfi  29935  wspthnfi  29948  wspthnonfi  29951  clwwlknfi  30073  qerclwwlknfi  30101  clwlknon2num  30396  numclwlk1lem2  30398  fsuppinisegfi  32701  offinsupp1  32744  fsumiunle  32835  elrgspnlem2  33232  elrgspnlem4  33234  elrspunidl  33435  elrspunsn  33436  rprmdvdsprod  33541  fedgmullem1  33656  constrfin  33750  hashreprin  34613  reprfi2  34616  hgt750lema  34650  tgoldbachgtde  34653  aks4d1p4  42060  aks4d1p5  42061  aks4d1p7  42064  aks4d1p8  42068  evl1gprodd  42098  hashscontpowcl  42101  idomnnzgmulnz  42114  deg1gprod  42121  sticksstones3  42129  sticksstones22  42149  aks6d1c6lem5  42158  grpods  42175  unitscyglem1  42176  unitscyglem2  42177  unitscyglem4  42179  unitscyglem5  42180  selvvvval  42571  cantnfub  43310  naddcnff  43351  fprodcnlem  45554  cnrefiisplem  45784  dvmptfprod  45900  dvnprodlem1  45901  sge0uzfsumgt  46399  hoidmvlelem1  46550  hoidmvlelem2  46551  hoidmvlelem3  46552  hoidmvlelem4  46553  hspmbllem1  46581