Theorem ssfid 8592

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

Syntax hints:   → wi 4   ∈ wcel 2081   ⊆ wss 3863  Fincfn 8362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5099  ax-nul 5106  ax-pow 5162  ax-pr 5226  ax-un 7324

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3710  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-pss 3880  df-nul 4216  df-if 4386  df-pw 4459  df-sn 4477  df-pr 4479  df-tp 4481  df-op 4483  df-uni 4750  df-br 4967  df-opab 5029  df-tr 5069  df-id 5353  df-eprel 5358  df-po 5367  df-so 5368  df-fr 5407  df-we 5409  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-rn 5459  df-res 5460  df-ima 5461  df-ord 6074  df-on 6075  df-lim 6076  df-suc 6077  df-fun 6232  df-fn 6233  df-f 6234  df-f1 6235  df-fo 6236  df-f1o 6237  df-om 7442  df-er 8144  df-en 8363  df-fin 8366

This theorem is referenced by:  ixpfi  8672  fisuppfi  8692  fsuppunbi  8705  ressuppfi  8710  fsuppmptif  8714  fsuppco2  8717  fsuppcor  8718  marypha1lem  8748  wemapso2lem  8867  cantnfp1lem1  8992  pwfseqlem4  9935  hashbclem  13663  hashf1lem2  13667  isercolllem2  14861  isercoll  14863  fsum2dlem  14963  fsumcom2  14967  fsumless  14989  fsumabs  14994  fsumrlim  15004  fsumo1  15005  fsumiun  15014  qshash  15020  incexc  15030  incexc2  15031  fprod2dlem  15172  fprodcom2  15176  4sqlem11  16125  vdwlem11  16161  ramlb  16189  0ram  16190  ramub1lem1  16196  ramub1lem2  16197  prmgaplem4  16224  isstruct2  16327  lagsubg2  18099  lagsubg  18100  orbsta2  18190  symgbasfi  18250  oddvds2  18428  sylow1lem3  18460  sylow1lem4  18461  sylow1lem5  18462  odcau  18464  pgpssslw  18474  sylow2alem2  18478  sylow2a  18479  sylow2blem1  18480  sylow2blem3  18482  slwhash  18484  fislw  18485  sylow2  18486  sylow3lem1  18487  sylow3lem3  18489  sylow3lem4  18490  sylow3lem6  18492  cyggenod  18731  gsumval3lem2  18752  gsumzadd  18767  gsum2dlem1  18815  gsum2dlem2  18816  gsum2d  18817  gsum2d2lem  18818  dprdfadd  18864  ablfac1eu  18917  pgpfac1lem5  18923  pgpfaclem2  18926  pgpfaclem3  18927  ablfaclem3  18931  lcomfsupp  19369  psrbaglecl  19842  psrbagaddcl  19843  psrbagcon  19844  mplcoe5  19941  dsmmacl  20572  dsmmsubg  20574  dsmmlss  20575  frlmsslsp  20627  mamures  20688  mdetrlin  20900  mdetrsca  20901  mdetralt  20906  madugsum  20941  fin1aufil  22229  xrge0gsumle  23129  xrge0tsms  23130  fsumcn  23166  rrxcph  23683  rrxmval  23696  i1fadd  23984  i1fmul  23985  i1fmulc  23992  i1fres  23994  mbfi1fseqlem4  24007  itgfsum  24115  dvmptfsum  24260  jensenlem1  25251  jensenlem2  25252  jensen  25253  0sgm  25408  sgmf  25409  sgmnncl  25411  fsumdvdsdiag  25448  fsumdvdscom  25449  dvdsflsumcom  25452  musum  25455  musumsum  25456  muinv  25457  fsumdvdsmul  25459  vmasum  25479  perfectlem2  25493  dchrfi  25518  rplogsumlem2  25748  rpvmasumlem  25750  dchrvmasumlem1  25758  dchrisum0ff  25770  dchrisum0  25783  vmalogdivsum2  25801  logsqvma  25805  logsqvma2  25806  selberg  25811  selberg34r  25834  pntsval2  25839  pntrlog2bndlem1  25840  wwlksnfi  27376  wspthnfi  27390  wspthnonfi  27393  clwwlknfi  27515  clwwlknfiOLD  27516  qerclwwlknfi  27544  clwlknon2num  27844  numclwlk1lem2  27846  offinsupp1  30156  fsumiunle  30234  fedgmullem1  30634  hashreprin  31513  reprfi2  31516  hgt750lema  31550  tgoldbachgtde  31553  phphashd  40080  prmgrpsimpgd  40197  fprodcnlem  41448  cnrefiisplem  41678  sge0uzfsumgt  42295  hoidmvlelem1  42446  hoidmvlelem2  42447  hoidmvlelem3  42448  hoidmvlelem4  42449  hspmbllem1  42477