Theorem ssfid 9288

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ⊆ wss 3900  Fincfn 9001

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-un 7775

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-om 7902  df-1o 8504  df-en 9002  df-fin 9005

This theorem is used by:  ixpfi  9366  fisuppfi  9391  finnzfsuppd  9392  fsuppunbi  9408  ressuppfi  9414  fsuppmptif  9418  fsuppco2  9422  fsuppcor  9423  marypha1lem  9452  wemapso2lem  9573  cantnfp1lem1  9706  pwfseqlem4  10774  hashpss  14581  hashbclem  14624  hashf1lem2  14628  phphashd  14638  isercolllem2  15862  isercoll  15864  fsum2dlem  15965  fsumcom2  15969  fsumless  15992  fsumabs  15997  fsumrlim  16007  fsumo1  16008  fsumiun  16017  qshash  16023  incexc  16035  incexc2  16036  fprod2dlem  16176  fprodcom2  16180  dvdsfi  16995  4sqlem11  17162  vdwlem11  17198  ramlb  17226  0ram  17227  ramub1lem1  17233  ramub1lem2  17234  prmgaplem4  17261  isstruct2  17356  lagsubg2  19438  lagsubg  19439  orbsta2  19558  symgbasfi  19623  oddvds2  19810  sylow1lem3  19844  sylow1lem4  19845  sylow1lem5  19846  odcau  19848  pgpssslw  19858  sylow2alem2  19862  sylow2a  19863  sylow2blem1  19864  sylow2blem3  19866  slwhash  19868  fislw  19869  sylow2  19870  sylow3lem1  19871  sylow3lem3  19873  sylow3lem4  19874  sylow3lem6  19876  cyggenod  20128  gsumval3lem2  20150  gsumzadd  20166  gsum2dlem1  20214  gsum2dlem2  20215  gsum2d  20216  gsum2d2lem  20217  dprdfadd  20266  ablfac1eu  20319  pgpfac1lem5  20325  pgpfaclem2  20328  pgpfaclem3  20329  ablfaclem3  20333  prmgrpsimpgd  20360  lcomfsupp  21207  dsmmacl  22077  dsmmsubg  22079  dsmmlss  22080  frlmsslsp  22132  psrbaglecl  22261  psrbagaddcl  22262  psrbagcon  22263  mplcoe5  22379  selvvvval  22481  mhpmulcl  22500  psdmplcl  22513  psdmul  22517  mamures  22742  mdetrlin  22947  mdetrsca  22948  mdetralt  22953  madugsum  22988  fin1aufil  24281  xrge0gsumle  25183  xrge0tsms  25184  fsumcn  25221  rrxcph  25743  rrxmval  25756  i1fadd  26046  i1fmul  26047  i1fmulc  26054  i1fres  26056  mbfi1fseqlem4  26069  itgfsum  26177  dvmptfsum  26325  plyconz  26661  jensenlem1  27344  jensenlem2  27345  jensen  27346  sgmf  27502  sgmnncl  27504  fsumdvdsdiag  27541  fsumdvdscom  27542  dvdsflsumcom  27545  musum  27548  musumsum  27549  muinv  27550  fsumdvdsmul  27552  perfectlem2  27587  dchrfi  27612  rplogsumlem2  27842  rpvmasumlem  27844  dchrvmasumlem1  27852  dchrisum0ff  27864  dchrisum0  27877  vmalogdivsum2  27895  logsqvma  27899  selberg  27905  selberg34r  27928  pntsval2  27933  pntrlog2bndlem1  27934  onsfi  28772  wwlksnfi  30525  wspthnfi  30538  wspthnonfi  30541  clwwlknfi  30666  qerclwwlknfi  30694  clwlknon2num  30999  numclwlk1lem2  31001  fsuppinisegfi  33351  offinsupp1  33388  fsumiunle  33490  elrgspnlem2  33874  elrgspnlem4  33876  elrgspnsubrunlem2  33879  domnprodeq0  33910  elrspunidl  34048  elrspunsn  34049  rprmdvdsprod  34136  deg1prod  34185  mplidomlem  34229  psrgsum  34250  psrmonprod  34254  esplyfval2  34267  esplymhp  34270  esplyind  34277  esplyindfv  34278  esplyfvn  34279  vieta  34282  exsslsb  34299  fedgmullem1  34331  fldextrspunlsplem  34375  constrfin  34448  hashreprin  35319  reprfi2  35322  hgt750lema  35356  tgoldbachgtde  35359  kardnnfi  35937  aks4d1p4  43321  aks4d1p5  43322  aks4d1p7  43325  aks4d1p8  43329  evl1gprodd  43359  hashscontpowcl  43362  idomnnzgmulnz  43375  deg1gprod  43382  sticksstones3  43390  sticksstones22  43410  aks6d1c6lem5  43419  grpods  43436  unitscyglem1  43437  unitscyglem2  43438  unitscyglem4  43440  unitscyglem5  43441  frlmnzcoordcl  43848  frlmnzcoordn0  43850  cantnfub  44515  naddcnff  44556  fprodcnlem  46816  sumnnodd  46847  cnrefiisplem  47044  dvmptfprod  47160  dvnprodlem1  47161  sge0uzfsumgt  47659  hoidmvlelem1  47810  hoidmvlelem2  47811  hoidmvlelem3  47812  hoidmvlelem4  47813  hspmbllem1  47841