Theorem ssfid 9212

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3914  Fincfn 8918

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-om 7843  df-1o 8434  df-en 8919  df-fin 8922

This theorem is referenced by:  ixpfi  9300  fisuppfi  9322  finnzfsuppd  9324  fsuppunbi  9340  ressuppfi  9346  fsuppmptif  9350  fsuppco2  9354  fsuppcor  9355  marypha1lem  9384  wemapso2lem  9505  cantnfp1lem1  9631  pwfseqlem4  10615  hashbclem  14417  hashf1lem2  14421  phphashd  14431  isercolllem2  15632  isercoll  15634  fsum2dlem  15736  fsumcom2  15740  fsumless  15762  fsumabs  15767  fsumrlim  15777  fsumo1  15778  fsumiun  15787  qshash  15793  incexc  15803  incexc2  15804  fprod2dlem  15946  fprodcom2  15950  dvdsfi  16759  4sqlem11  16926  vdwlem11  16962  ramlb  16990  0ram  16991  ramub1lem1  16997  ramub1lem2  16998  prmgaplem4  17025  isstruct2  17119  lagsubg2  19126  lagsubg  19127  orbsta2  19246  symgbasfi  19309  oddvds2  19496  sylow1lem3  19530  sylow1lem4  19531  sylow1lem5  19532  odcau  19534  pgpssslw  19544  sylow2alem2  19548  sylow2a  19549  sylow2blem1  19550  sylow2blem3  19552  slwhash  19554  fislw  19555  sylow2  19556  sylow3lem1  19557  sylow3lem3  19559  sylow3lem4  19560  sylow3lem6  19562  cyggenod  19814  gsumval3lem2  19836  gsumzadd  19852  gsum2dlem1  19900  gsum2dlem2  19901  gsum2d  19902  gsum2d2lem  19903  dprdfadd  19952  ablfac1eu  20005  pgpfac1lem5  20011  pgpfaclem2  20014  pgpfaclem3  20015  ablfaclem3  20019  prmgrpsimpgd  20046  lcomfsupp  20808  dsmmacl  21650  dsmmsubg  21652  dsmmlss  21653  frlmsslsp  21705  psrbaglecl  21832  psrbagaddcl  21833  psrbagcon  21834  mplcoe5  21947  mhpmulcl  22036  psdmplcl  22049  psdmul  22053  mamures  22284  mdetrlin  22489  mdetrsca  22490  mdetralt  22495  madugsum  22530  fin1aufil  23819  xrge0gsumle  24722  xrge0tsms  24723  fsumcn  24761  rrxcph  25292  rrxmval  25305  i1fadd  25596  i1fmul  25597  i1fmulc  25604  i1fres  25606  mbfi1fseqlem4  25619  itgfsum  25728  dvmptfsum  25879  jensenlem1  26897  jensenlem2  26898  jensen  26899  sgmf  27055  sgmnncl  27057  fsumdvdsdiag  27094  fsumdvdscom  27095  dvdsflsumcom  27098  musum  27101  musumsum  27102  muinv  27103  fsumdvdsmul  27105  fsumdvdsmulOLD  27107  perfectlem2  27141  dchrfi  27166  rplogsumlem2  27396  rpvmasumlem  27398  dchrvmasumlem1  27406  dchrisum0ff  27418  dchrisum0  27431  vmalogdivsum2  27449  logsqvma  27453  selberg  27459  selberg34r  27482  pntsval2  27487  pntrlog2bndlem1  27488  onsfi  28247  wwlksnfi  29836  wspthnfi  29849  wspthnonfi  29852  clwwlknfi  29974  qerclwwlknfi  30002  clwlknon2num  30297  numclwlk1lem2  30299  fsuppinisegfi  32610  offinsupp1  32650  hashpss  32734  fsumiunle  32754  elrgspnlem2  33194  elrgspnlem4  33196  elrgspnsubrunlem2  33199  elrspunidl  33399  elrspunsn  33400  rprmdvdsprod  33505  exsslsb  33592  fedgmullem1  33625  fldextrspunlsplem  33668  constrfin  33736  hashreprin  34611  reprfi2  34614  hgt750lema  34648  tgoldbachgtde  34651  aks4d1p4  42067  aks4d1p5  42068  aks4d1p7  42071  aks4d1p8  42075  evl1gprodd  42105  hashscontpowcl  42108  idomnnzgmulnz  42121  deg1gprod  42128  sticksstones3  42136  sticksstones22  42156  aks6d1c6lem5  42165  grpods  42182  unitscyglem1  42183  unitscyglem2  42184  unitscyglem4  42186  unitscyglem5  42187  selvvvval  42573  cantnfub  43310  naddcnff  43351  fprodcnlem  45597  cnrefiisplem  45827  dvmptfprod  45943  dvnprodlem1  45944  sge0uzfsumgt  46442  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvlelem4  46596  hspmbllem1  46624