Theorem ssfid 9219

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3917  Fincfn 8921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-om 7846  df-1o 8437  df-en 8922  df-fin 8925

This theorem is referenced by:  ixpfi  9307  fisuppfi  9329  finnzfsuppd  9331  fsuppunbi  9347  ressuppfi  9353  fsuppmptif  9357  fsuppco2  9361  fsuppcor  9362  marypha1lem  9391  wemapso2lem  9512  cantnfp1lem1  9638  pwfseqlem4  10622  hashbclem  14424  hashf1lem2  14428  phphashd  14438  isercolllem2  15639  isercoll  15641  fsum2dlem  15743  fsumcom2  15747  fsumless  15769  fsumabs  15774  fsumrlim  15784  fsumo1  15785  fsumiun  15794  qshash  15800  incexc  15810  incexc2  15811  fprod2dlem  15953  fprodcom2  15957  dvdsfi  16766  4sqlem11  16933  vdwlem11  16969  ramlb  16997  0ram  16998  ramub1lem1  17004  ramub1lem2  17005  prmgaplem4  17032  isstruct2  17126  lagsubg2  19133  lagsubg  19134  orbsta2  19253  symgbasfi  19316  oddvds2  19503  sylow1lem3  19537  sylow1lem4  19538  sylow1lem5  19539  odcau  19541  pgpssslw  19551  sylow2alem2  19555  sylow2a  19556  sylow2blem1  19557  sylow2blem3  19559  slwhash  19561  fislw  19562  sylow2  19563  sylow3lem1  19564  sylow3lem3  19566  sylow3lem4  19567  sylow3lem6  19569  cyggenod  19821  gsumval3lem2  19843  gsumzadd  19859  gsum2dlem1  19907  gsum2dlem2  19908  gsum2d  19909  gsum2d2lem  19910  dprdfadd  19959  ablfac1eu  20012  pgpfac1lem5  20018  pgpfaclem2  20021  pgpfaclem3  20022  ablfaclem3  20026  prmgrpsimpgd  20053  lcomfsupp  20815  dsmmacl  21657  dsmmsubg  21659  dsmmlss  21660  frlmsslsp  21712  psrbaglecl  21839  psrbagaddcl  21840  psrbagcon  21841  mplcoe5  21954  mhpmulcl  22043  psdmplcl  22056  psdmul  22060  mamures  22291  mdetrlin  22496  mdetrsca  22497  mdetralt  22502  madugsum  22537  fin1aufil  23826  xrge0gsumle  24729  xrge0tsms  24730  fsumcn  24768  rrxcph  25299  rrxmval  25312  i1fadd  25603  i1fmul  25604  i1fmulc  25611  i1fres  25613  mbfi1fseqlem4  25626  itgfsum  25735  dvmptfsum  25886  jensenlem1  26904  jensenlem2  26905  jensen  26906  sgmf  27062  sgmnncl  27064  fsumdvdsdiag  27101  fsumdvdscom  27102  dvdsflsumcom  27105  musum  27108  musumsum  27109  muinv  27110  fsumdvdsmul  27112  fsumdvdsmulOLD  27114  perfectlem2  27148  dchrfi  27173  rplogsumlem2  27403  rpvmasumlem  27405  dchrvmasumlem1  27413  dchrisum0ff  27425  dchrisum0  27438  vmalogdivsum2  27456  logsqvma  27460  selberg  27466  selberg34r  27489  pntsval2  27494  pntrlog2bndlem1  27495  onsfi  28254  wwlksnfi  29843  wspthnfi  29856  wspthnonfi  29859  clwwlknfi  29981  qerclwwlknfi  30009  clwlknon2num  30304  numclwlk1lem2  30306  fsuppinisegfi  32617  offinsupp1  32657  hashpss  32741  fsumiunle  32761  elrgspnlem2  33201  elrgspnlem4  33203  elrgspnsubrunlem2  33206  elrspunidl  33406  elrspunsn  33407  rprmdvdsprod  33512  exsslsb  33599  fedgmullem1  33632  fldextrspunlsplem  33675  constrfin  33743  hashreprin  34618  reprfi2  34621  hgt750lema  34655  tgoldbachgtde  34658  aks4d1p4  42074  aks4d1p5  42075  aks4d1p7  42078  aks4d1p8  42082  evl1gprodd  42112  hashscontpowcl  42115  idomnnzgmulnz  42128  deg1gprod  42135  sticksstones3  42143  sticksstones22  42163  aks6d1c6lem5  42172  grpods  42189  unitscyglem1  42190  unitscyglem2  42191  unitscyglem4  42193  unitscyglem5  42194  selvvvval  42580  cantnfub  43317  naddcnff  43358  fprodcnlem  45604  cnrefiisplem  45834  dvmptfprod  45950  dvnprodlem1  45951  sge0uzfsumgt  46449  hoidmvlelem1  46600  hoidmvlelem2  46601  hoidmvlelem3  46602  hoidmvlelem4  46603  hspmbllem1  46631