Theorem ssfid 9003

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3891  Fincfn 8707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355  ax-un 7579

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3072  df-rab 3074  df-v 3432  df-sbc 3720  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-pss 3910  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4845  df-br 5079  df-opab 5141  df-tr 5196  df-id 5488  df-eprel 5494  df-po 5502  df-so 5503  df-fr 5543  df-we 5545  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-ord 6266  df-on 6267  df-lim 6268  df-suc 6269  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-om 7701  df-1o 8281  df-en 8708  df-fin 8711

This theorem is referenced by:  ixpfi  9077  fisuppfi  9097  fsuppunbi  9110  ressuppfi  9115  fsuppmptif  9119  fsuppco2  9123  fsuppcor  9124  marypha1lem  9153  wemapso2lem  9272  cantnfp1lem1  9397  pwfseqlem4  10402  hashbclem  14145  hashf1lem2  14151  phphashd  14161  isercolllem2  15358  isercoll  15360  fsum2dlem  15463  fsumcom2  15467  fsumless  15489  fsumabs  15494  fsumrlim  15504  fsumo1  15505  fsumiun  15514  qshash  15520  incexc  15530  incexc2  15531  fprod2dlem  15671  fprodcom2  15675  4sqlem11  16637  vdwlem11  16673  ramlb  16701  0ram  16702  ramub1lem1  16708  ramub1lem2  16709  prmgaplem4  16736  isstruct2  16831  lagsubg2  18798  lagsubg  18799  orbsta2  18901  symgbasfi  18967  oddvds2  19154  sylow1lem3  19186  sylow1lem4  19187  sylow1lem5  19188  odcau  19190  pgpssslw  19200  sylow2alem2  19204  sylow2a  19205  sylow2blem1  19206  sylow2blem3  19208  slwhash  19210  fislw  19211  sylow2  19212  sylow3lem1  19213  sylow3lem3  19215  sylow3lem4  19216  sylow3lem6  19218  cyggenod  19465  gsumval3lem2  19488  gsumzadd  19504  gsum2dlem1  19552  gsum2dlem2  19553  gsum2d  19554  gsum2d2lem  19555  dprdfadd  19604  ablfac1eu  19657  pgpfac1lem5  19663  pgpfaclem2  19666  pgpfaclem3  19667  ablfaclem3  19671  prmgrpsimpgd  19698  lcomfsupp  20144  dsmmacl  20929  dsmmsubg  20931  dsmmlss  20932  frlmsslsp  20984  psrbaglecl  21110  psrbagleclOLD  21111  psrbagaddcl  21112  psrbagaddclOLD  21113  psrbagcon  21114  psrbagconOLD  21115  mplcoe5  21222  mhpmulcl  21320  mamures  21520  mdetrlin  21732  mdetrsca  21733  mdetralt  21738  madugsum  21773  fin1aufil  23064  xrge0gsumle  23977  xrge0tsms  23978  fsumcn  24014  rrxcph  24537  rrxmval  24550  i1fadd  24840  i1fmul  24841  i1fmulc  24849  i1fres  24851  mbfi1fseqlem4  24864  itgfsum  24972  dvmptfsum  25120  jensenlem1  26117  jensenlem2  26118  jensen  26119  0sgm  26274  sgmf  26275  sgmnncl  26277  fsumdvdsdiag  26314  fsumdvdscom  26315  dvdsflsumcom  26318  musum  26321  musumsum  26322  muinv  26323  fsumdvdsmul  26325  vmasum  26345  perfectlem2  26359  dchrfi  26384  rplogsumlem2  26614  rpvmasumlem  26616  dchrvmasumlem1  26624  dchrisum0ff  26636  dchrisum0  26649  vmalogdivsum2  26667  logsqvma  26671  logsqvma2  26672  selberg  26677  selberg34r  26700  pntsval2  26705  pntrlog2bndlem1  26706  wwlksnfi  28250  wspthnfi  28263  wspthnonfi  28266  clwwlknfi  28388  qerclwwlknfi  28416  clwlknon2num  28711  numclwlk1lem2  28713  fsuppinisegfi  31000  offinsupp1  31041  fsumiunle  31122  elrspunidl  31585  fedgmullem1  31689  hashreprin  32579  reprfi2  32582  hgt750lema  32616  tgoldbachgtde  32619  aks4d1p4  40067  aks4d1p5  40068  aks4d1p7  40071  aks4d1p8  40075  sticksstones3  40084  sticksstones22  40104  evlsbagval  40255  mhphf  40265  finnzfsuppd  41773  fprodcnlem  43094  cnrefiisplem  43324  sge0uzfsumgt  43936  hoidmvlelem1  44087  hoidmvlelem2  44088  hoidmvlelem3  44089  hoidmvlelem4  44090  hspmbllem1  44118