Theorem ssfid 9242

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3902  Fincfn 8955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402  ax-un 7739

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-om 7866  df-1o 8458  df-en 8956  df-fin 8959

This theorem is used by:  ixpfi  9319  fisuppfi  9344  finnzfsuppd  9346  fsuppunbi  9362  ressuppfi  9368  fsuppmptif  9372  fsuppco2  9376  fsuppcor  9377  marypha1lem  9406  wemapso2lem  9527  cantnfp1lem1  9660  pwfseqlem4  10674  hashpss  14476  hashbclem  14519  hashf1lem2  14523  phphashd  14533  isercolllem2  15755  isercoll  15757  fsum2dlem  15858  fsumcom2  15862  fsumless  15885  fsumabs  15890  fsumrlim  15900  fsumo1  15901  fsumiun  15910  qshash  15916  incexc  15928  incexc2  15929  fprod2dlem  16071  fprodcom2  16075  dvdsfi  16884  4sqlem11  17051  vdwlem11  17087  ramlb  17115  0ram  17116  ramub1lem1  17122  ramub1lem2  17123  prmgaplem4  17150  isstruct2  17245  lagsubg2  19323  lagsubg  19324  orbsta2  19442  symgbasfi  19507  oddvds2  19694  sylow1lem3  19728  sylow1lem4  19729  sylow1lem5  19730  odcau  19732  pgpssslw  19742  sylow2alem2  19746  sylow2a  19747  sylow2blem1  19748  sylow2blem3  19750  slwhash  19752  fislw  19753  sylow2  19754  sylow3lem1  19755  sylow3lem3  19757  sylow3lem4  19758  sylow3lem6  19760  cyggenod  20012  gsumval3lem2  20034  gsumzadd  20050  gsum2dlem1  20098  gsum2dlem2  20099  gsum2d  20100  gsum2d2lem  20101  dprdfadd  20150  ablfac1eu  20203  pgpfac1lem5  20209  pgpfaclem2  20212  pgpfaclem3  20213  ablfaclem3  20217  prmgrpsimpgd  20244  lcomfsupp  21087  dsmmacl  21955  dsmmsubg  21957  dsmmlss  21958  frlmsslsp  22010  psrbaglecl  22139  psrbagaddcl  22140  psrbagcon  22141  mplcoe5  22257  selvvvval  22359  mhpmulcl  22378  psdmplcl  22391  psdmul  22395  mamures  22620  mdetrlin  22825  mdetrsca  22826  mdetralt  22831  madugsum  22866  fin1aufil  24159  xrge0gsumle  25061  xrge0tsms  25062  fsumcn  25099  rrxcph  25621  rrxmval  25634  i1fadd  25924  i1fmul  25925  i1fmulc  25932  i1fres  25934  mbfi1fseqlem4  25947  itgfsum  26056  dvmptfsum  26204  jensenlem1  27221  jensenlem2  27222  jensen  27223  sgmf  27379  sgmnncl  27381  fsumdvdsdiag  27418  fsumdvdscom  27419  dvdsflsumcom  27422  musum  27425  musumsum  27426  muinv  27427  fsumdvdsmul  27429  perfectlem2  27464  dchrfi  27489  rplogsumlem2  27719  rpvmasumlem  27721  dchrvmasumlem1  27729  dchrisum0ff  27741  dchrisum0  27754  vmalogdivsum2  27772  logsqvma  27776  selberg  27782  selberg34r  27805  pntsval2  27810  pntrlog2bndlem1  27811  onsfi  28619  wwlksnfi  30360  wspthnfi  30373  wspthnonfi  30376  clwwlknfi  30501  qerclwwlknfi  30529  clwlknon2num  30834  numclwlk1lem2  30836  fsuppinisegfi  33146  offinsupp1  33184  fsumiunle  33286  elrgspnlem2  33670  elrgspnlem4  33672  elrgspnsubrunlem2  33675  domnprodeq0  33706  elrspunidl  33843  elrspunsn  33844  rprmdvdsprod  33931  deg1prod  33980  mplidomlem  34024  psrgsum  34045  psrmonprod  34049  esplyfval2  34062  esplymhp  34065  esplyind  34072  esplyindfv  34073  esplyfvn  34074  vieta  34077  exsslsb  34094  fedgmullem1  34126  fldextrspunlsplem  34170  constrfin  34243  hashreprin  35115  reprfi2  35118  hgt750lema  35152  tgoldbachgtde  35155  kardnnfi  35682  aks4d1p4  42932  aks4d1p5  42933  aks4d1p7  42936  aks4d1p8  42940  evl1gprodd  42970  hashscontpowcl  42973  idomnnzgmulnz  42986  deg1gprod  42993  sticksstones3  43001  sticksstones22  43021  aks6d1c6lem5  43030  grpods  43047  unitscyglem1  43048  unitscyglem2  43049  unitscyglem4  43051  unitscyglem5  43052  cantnfub  44149  naddcnff  44190  fprodcnlem  46416  cnrefiisplem  46644  dvmptfprod  46760  dvnprodlem1  46761  sge0uzfsumgt  47259  hoidmvlelem1  47410  hoidmvlelem2  47411  hoidmvlelem3  47412  hoidmvlelem4  47413  hspmbllem1  47441