Theorem ssfid 9228

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

Syntax hints:   → wi 4   ∈ wcel 2141   ⊆ wss 3904  Fincfn 8942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5256  ax-nul 5268  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3744  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-tr 5218  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 7862  df-1o 8452  df-en 8943  df-fin 8946

This theorem is referenced by:  ixpfi  9305  fisuppfi  9330  finnzfsuppd  9332  fsuppunbi  9348  ressuppfi  9354  fsuppmptif  9358  fsuppco2  9362  fsuppcor  9363  marypha1lem  9392  wemapso2lem  9513  cantnfp1lem1  9646  pwfseqlem4  10646  hashpss  14445  hashbclem  14488  hashf1lem2  14492  phphashd  14502  isercolllem2  15716  isercoll  15718  fsum2dlem  15820  fsumcom2  15824  fsumless  15847  fsumabs  15852  fsumrlim  15862  fsumo1  15863  fsumiun  15872  qshash  15878  incexc  15890  incexc2  15891  fprod2dlem  16033  fprodcom2  16037  dvdsfi  16847  4sqlem11  17014  vdwlem11  17050  ramlb  17078  0ram  17079  ramub1lem1  17085  ramub1lem2  17086  prmgaplem4  17113  isstruct2  17208  lagsubg2  19264  lagsubg  19265  orbsta2  19383  symgbasfi  19448  oddvds2  19635  sylow1lem3  19669  sylow1lem4  19670  sylow1lem5  19671  odcau  19673  pgpssslw  19683  sylow2alem2  19687  sylow2a  19688  sylow2blem1  19689  sylow2blem3  19691  slwhash  19693  fislw  19694  sylow2  19695  sylow3lem1  19696  sylow3lem3  19698  sylow3lem4  19699  sylow3lem6  19701  cyggenod  19953  gsumval3lem2  19975  gsumzadd  19991  gsum2dlem1  20039  gsum2dlem2  20040  gsum2d  20041  gsum2d2lem  20042  dprdfadd  20091  ablfac1eu  20144  pgpfac1lem5  20150  pgpfaclem2  20153  pgpfaclem3  20154  ablfaclem3  20158  prmgrpsimpgd  20185  lcomfsupp  21002  dsmmacl  21870  dsmmsubg  21872  dsmmlss  21873  frlmsslsp  21925  psrbaglecl  22052  psrbagaddcl  22053  psrbagcon  22054  mplcoe5  22170  selvvvval  22272  mhpmulcl  22291  psdmplcl  22304  psdmul  22308  mamures  22533  mdetrlin  22738  mdetrsca  22739  mdetralt  22744  madugsum  22779  fin1aufil  24068  xrge0gsumle  24970  xrge0tsms  24971  fsumcn  25008  rrxcph  25530  rrxmval  25543  i1fadd  25833  i1fmul  25834  i1fmulc  25841  i1fres  25843  mbfi1fseqlem4  25856  itgfsum  25965  dvmptfsum  26113  jensenlem1  27127  jensenlem2  27128  jensen  27129  sgmf  27285  sgmnncl  27287  fsumdvdsdiag  27324  fsumdvdscom  27325  dvdsflsumcom  27328  musum  27331  musumsum  27332  muinv  27333  fsumdvdsmul  27335  perfectlem2  27370  dchrfi  27395  rplogsumlem2  27625  rpvmasumlem  27627  dchrvmasumlem1  27635  dchrisum0ff  27647  dchrisum0  27660  vmalogdivsum2  27678  logsqvma  27682  selberg  27688  selberg34r  27711  pntsval2  27716  pntrlog2bndlem1  27717  onsfi  28525  wwlksnfi  30221  wspthnfi  30234  wspthnonfi  30237  clwwlknfi  30362  qerclwwlknfi  30390  clwlknon2num  30685  numclwlk1lem2  30687  fsuppinisegfi  32998  offinsupp1  33037  fsumiunle  33139  elrgspnlem2  33529  elrgspnlem4  33531  elrgspnsubrunlem2  33534  domnprodeq0  33565  elrspunidl  33702  elrspunsn  33703  rprmdvdsprod  33790  deg1prod  33839  mplidomlem  33883  psrgsum  33904  psrmonprod  33908  esplyfval2  33921  esplymhp  33924  esplyind  33931  esplyindfv  33932  esplyfvn  33933  vieta  33936  exsslsb  33953  fedgmullem1  33985  fldextrspunlsplem  34029  constrfin  34102  hashreprin  34973  reprfi2  34976  hgt750lema  35010  tgoldbachgtde  35013  kardnnfi  35536  aks4d1p4  42792  aks4d1p5  42793  aks4d1p7  42796  aks4d1p8  42800  evl1gprodd  42830  hashscontpowcl  42833  idomnnzgmulnz  42846  deg1gprod  42853  sticksstones3  42861  sticksstones22  42881  aks6d1c6lem5  42890  grpods  42907  unitscyglem1  42908  unitscyglem2  42909  unitscyglem4  42911  unitscyglem5  42912  cantnfub  43996  naddcnff  44037  fprodcnlem  46263  cnrefiisplem  46491  dvmptfprod  46607  dvnprodlem1  46608  sge0uzfsumgt  47106  hoidmvlelem1  47257  hoidmvlelem2  47258  hoidmvlelem3  47259  hoidmvlelem4  47260  hspmbllem1  47288