Theorem ssfid 9225

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2143   ⊆ wss 3905  Fincfn 8939

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-un 7732

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-om 7859  df-1o 8449  df-en 8940  df-fin 8943

This theorem is used by:  ixpfi  9302  fisuppfi  9327  finnzfsuppd  9329  fsuppunbi  9345  ressuppfi  9351  fsuppmptif  9355  fsuppco2  9359  fsuppcor  9360  marypha1lem  9389  wemapso2lem  9510  cantnfp1lem1  9643  pwfseqlem4  10651  hashpss  14451  hashbclem  14494  hashf1lem2  14498  phphashd  14508  isercolllem2  15722  isercoll  15724  fsum2dlem  15826  fsumcom2  15830  fsumless  15853  fsumabs  15858  fsumrlim  15868  fsumo1  15869  fsumiun  15878  qshash  15884  incexc  15896  incexc2  15897  fprod2dlem  16039  fprodcom2  16043  dvdsfi  16852  4sqlem11  17019  vdwlem11  17055  ramlb  17083  0ram  17084  ramub1lem1  17090  ramub1lem2  17091  prmgaplem4  17118  isstruct2  17213  lagsubg2  19269  lagsubg  19270  orbsta2  19388  symgbasfi  19453  oddvds2  19640  sylow1lem3  19674  sylow1lem4  19675  sylow1lem5  19676  odcau  19678  pgpssslw  19688  sylow2alem2  19692  sylow2a  19693  sylow2blem1  19694  sylow2blem3  19696  slwhash  19698  fislw  19699  sylow2  19700  sylow3lem1  19701  sylow3lem3  19703  sylow3lem4  19704  sylow3lem6  19706  cyggenod  19958  gsumval3lem2  19980  gsumzadd  19996  gsum2dlem1  20044  gsum2dlem2  20045  gsum2d  20046  gsum2d2lem  20047  dprdfadd  20096  ablfac1eu  20149  pgpfac1lem5  20155  pgpfaclem2  20158  pgpfaclem3  20159  ablfaclem3  20163  prmgrpsimpgd  20190  lcomfsupp  21032  dsmmacl  21900  dsmmsubg  21902  dsmmlss  21903  frlmsslsp  21955  psrbaglecl  22082  psrbagaddcl  22083  psrbagcon  22084  mplcoe5  22200  selvvvval  22302  mhpmulcl  22321  psdmplcl  22334  psdmul  22338  mamures  22563  mdetrlin  22768  mdetrsca  22769  mdetralt  22774  madugsum  22809  fin1aufil  24098  xrge0gsumle  25000  xrge0tsms  25001  fsumcn  25038  rrxcph  25560  rrxmval  25573  i1fadd  25863  i1fmul  25864  i1fmulc  25871  i1fres  25873  mbfi1fseqlem4  25886  itgfsum  25995  dvmptfsum  26143  jensenlem1  27160  jensenlem2  27161  jensen  27162  sgmf  27318  sgmnncl  27320  fsumdvdsdiag  27357  fsumdvdscom  27358  dvdsflsumcom  27361  musum  27364  musumsum  27365  muinv  27366  fsumdvdsmul  27368  perfectlem2  27403  dchrfi  27428  rplogsumlem2  27658  rpvmasumlem  27660  dchrvmasumlem1  27668  dchrisum0ff  27680  dchrisum0  27693  vmalogdivsum2  27711  logsqvma  27715  selberg  27721  selberg34r  27744  pntsval2  27749  pntrlog2bndlem1  27750  onsfi  28558  wwlksnfi  30264  wspthnfi  30277  wspthnonfi  30280  clwwlknfi  30405  qerclwwlknfi  30433  clwlknon2num  30728  numclwlk1lem2  30730  fsuppinisegfi  33041  offinsupp1  33080  fsumiunle  33182  elrgspnlem2  33572  elrgspnlem4  33574  elrgspnsubrunlem2  33577  domnprodeq0  33608  elrspunidl  33745  elrspunsn  33746  rprmdvdsprod  33833  deg1prod  33882  mplidomlem  33926  psrgsum  33947  psrmonprod  33951  esplyfval2  33964  esplymhp  33967  esplyind  33974  esplyindfv  33975  esplyfvn  33976  vieta  33979  exsslsb  33996  fedgmullem1  34028  fldextrspunlsplem  34072  constrfin  34145  hashreprin  35016  reprfi2  35019  hgt750lema  35053  tgoldbachgtde  35056  kardnnfi  35590  aks4d1p4  42874  aks4d1p5  42875  aks4d1p7  42878  aks4d1p8  42882  evl1gprodd  42912  hashscontpowcl  42915  idomnnzgmulnz  42928  deg1gprod  42935  sticksstones3  42943  sticksstones22  42963  aks6d1c6lem5  42972  grpods  42989  unitscyglem1  42990  unitscyglem2  42991  unitscyglem4  42993  unitscyglem5  42994  cantnfub  44076  naddcnff  44117  fprodcnlem  46343  cnrefiisplem  46571  dvmptfprod  46687  dvnprodlem1  46688  sge0uzfsumgt  47186  hoidmvlelem1  47337  hoidmvlelem2  47338  hoidmvlelem3  47339  hoidmvlelem4  47340  hspmbllem1  47368