Theorem ssfid 8740

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

Syntax hints:   → wi 4   ∈ wcel 2110   ⊆ wss 3935  Fincfn 8508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pow 5265  ax-pr 5329  ax-un 7460

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4838  df-br 5066  df-opab 5128  df-tr 5172  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-om 7580  df-er 8288  df-en 8509  df-fin 8512

This theorem is referenced by:  ixpfi  8820  fisuppfi  8840  fsuppunbi  8853  ressuppfi  8858  fsuppmptif  8862  fsuppco2  8865  fsuppcor  8866  marypha1lem  8896  wemapso2lem  9015  cantnfp1lem1  9140  pwfseqlem4  10083  hashbclem  13809  hashf1lem2  13813  phphashd  13823  isercolllem2  15021  isercoll  15023  fsum2dlem  15124  fsumcom2  15128  fsumless  15150  fsumabs  15155  fsumrlim  15165  fsumo1  15166  fsumiun  15175  qshash  15181  incexc  15191  incexc2  15192  fprod2dlem  15333  fprodcom2  15337  4sqlem11  16290  vdwlem11  16326  ramlb  16354  0ram  16355  ramub1lem1  16361  ramub1lem2  16362  prmgaplem4  16389  isstruct2  16492  lagsubg2  18340  lagsubg  18341  orbsta2  18443  symgbasfi  18506  oddvds2  18692  sylow1lem3  18724  sylow1lem4  18725  sylow1lem5  18726  odcau  18728  pgpssslw  18738  sylow2alem2  18742  sylow2a  18743  sylow2blem1  18744  sylow2blem3  18746  slwhash  18748  fislw  18749  sylow2  18750  sylow3lem1  18751  sylow3lem3  18753  sylow3lem4  18754  sylow3lem6  18756  cyggenod  19002  gsumval3lem2  19025  gsumzadd  19041  gsum2dlem1  19089  gsum2dlem2  19090  gsum2d  19091  gsum2d2lem  19092  dprdfadd  19141  ablfac1eu  19194  pgpfac1lem5  19200  pgpfaclem2  19203  pgpfaclem3  19204  ablfaclem3  19208  prmgrpsimpgd  19235  lcomfsupp  19673  psrbaglecl  20148  psrbagaddcl  20149  psrbagcon  20150  mplcoe5  20248  dsmmacl  20884  dsmmsubg  20886  dsmmlss  20887  frlmsslsp  20939  mamures  21000  mdetrlin  21210  mdetrsca  21211  mdetralt  21216  madugsum  21251  fin1aufil  22539  xrge0gsumle  23440  xrge0tsms  23441  fsumcn  23477  rrxcph  23994  rrxmval  24007  i1fadd  24295  i1fmul  24296  i1fmulc  24303  i1fres  24305  mbfi1fseqlem4  24318  itgfsum  24426  dvmptfsum  24571  jensenlem1  25563  jensenlem2  25564  jensen  25565  0sgm  25720  sgmf  25721  sgmnncl  25723  fsumdvdsdiag  25760  fsumdvdscom  25761  dvdsflsumcom  25764  musum  25767  musumsum  25768  muinv  25769  fsumdvdsmul  25771  vmasum  25791  perfectlem2  25805  dchrfi  25830  rplogsumlem2  26060  rpvmasumlem  26062  dchrvmasumlem1  26070  dchrisum0ff  26082  dchrisum0  26095  vmalogdivsum2  26113  logsqvma  26117  logsqvma2  26118  selberg  26123  selberg34r  26146  pntsval2  26151  pntrlog2bndlem1  26152  wwlksnfi  27683  wspthnfi  27697  wspthnonfi  27700  clwwlknfi  27822  clwwlknfiOLD  27823  qerclwwlknfi  27851  clwlknon2num  28146  numclwlk1lem2  28148  offinsupp1  30462  fsumiunle  30545  fedgmullem1  31025  hashreprin  31891  reprfi2  31894  hgt750lema  31928  tgoldbachgtde  31931  fprodcnlem  41878  cnrefiisplem  42108  sge0uzfsumgt  42725  hoidmvlelem1  42876  hoidmvlelem2  42877  hoidmvlelem3  42878  hoidmvlelem4  42879  hspmbllem1  42907