Theorem ssfid 9238

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

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

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 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7734

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-ord 6354  df-on 6355  df-lim 6356  df-suc 6357  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-om 7861  df-1o 8454  df-en 8952  df-fin 8955

This theorem is used by:  ixpfi  9316  fisuppfi  9341  finnzfsuppd  9343  fsuppunbi  9359  ressuppfi  9365  fsuppmptif  9369  fsuppco2  9373  fsuppcor  9374  marypha1lem  9403  wemapso2lem  9524  cantnfp1lem1  9657  pwfseqlem4  10718  hashpss  14521  hashbclem  14564  hashf1lem2  14568  phphashd  14578  isercolllem2  15800  isercoll  15802  fsum2dlem  15903  fsumcom2  15907  fsumless  15930  fsumabs  15935  fsumrlim  15945  fsumo1  15946  fsumiun  15955  qshash  15961  incexc  15973  incexc2  15974  fprod2dlem  16114  fprodcom2  16118  dvdsfi  16927  4sqlem11  17094  vdwlem11  17130  ramlb  17158  0ram  17159  ramub1lem1  17165  ramub1lem2  17166  prmgaplem4  17193  isstruct2  17288  lagsubg2  19370  lagsubg  19371  orbsta2  19489  symgbasfi  19554  oddvds2  19741  sylow1lem3  19775  sylow1lem4  19776  sylow1lem5  19777  odcau  19779  pgpssslw  19789  sylow2alem2  19793  sylow2a  19794  sylow2blem1  19795  sylow2blem3  19797  slwhash  19799  fislw  19800  sylow2  19801  sylow3lem1  19802  sylow3lem3  19804  sylow3lem4  19805  sylow3lem6  19807  cyggenod  20059  gsumval3lem2  20081  gsumzadd  20097  gsum2dlem1  20145  gsum2dlem2  20146  gsum2d  20147  gsum2d2lem  20148  dprdfadd  20197  ablfac1eu  20250  pgpfac1lem5  20256  pgpfaclem2  20259  pgpfaclem3  20260  ablfaclem3  20264  prmgrpsimpgd  20291  lcomfsupp  21138  dsmmacl  22008  dsmmsubg  22010  dsmmlss  22011  frlmsslsp  22063  psrbaglecl  22192  psrbagaddcl  22193  psrbagcon  22194  mplcoe5  22310  selvvvval  22412  mhpmulcl  22431  psdmplcl  22444  psdmul  22448  mamures  22673  mdetrlin  22878  mdetrsca  22879  mdetralt  22884  madugsum  22919  fin1aufil  24212  xrge0gsumle  25114  xrge0tsms  25115  fsumcn  25152  rrxcph  25674  rrxmval  25687  i1fadd  25977  i1fmul  25978  i1fmulc  25985  i1fres  25987  mbfi1fseqlem4  26000  itgfsum  26108  dvmptfsum  26256  plyconz  26594  jensenlem1  27277  jensenlem2  27278  jensen  27279  sgmf  27435  sgmnncl  27437  fsumdvdsdiag  27474  fsumdvdscom  27475  dvdsflsumcom  27478  musum  27481  musumsum  27482  muinv  27483  fsumdvdsmul  27485  perfectlem2  27520  dchrfi  27545  rplogsumlem2  27775  rpvmasumlem  27777  dchrvmasumlem1  27785  dchrisum0ff  27797  dchrisum0  27810  vmalogdivsum2  27828  logsqvma  27832  selberg  27838  selberg34r  27861  pntsval2  27866  pntrlog2bndlem1  27867  onsfi  28675  wwlksnfi  30428  wspthnfi  30441  wspthnonfi  30444  clwwlknfi  30569  qerclwwlknfi  30597  clwlknon2num  30902  numclwlk1lem2  30904  fsuppinisegfi  33213  offinsupp1  33251  fsumiunle  33353  elrgspnlem2  33737  elrgspnlem4  33739  elrgspnsubrunlem2  33742  domnprodeq0  33773  elrspunidl  33911  elrspunsn  33912  rprmdvdsprod  33999  deg1prod  34048  mplidomlem  34092  psrgsum  34113  psrmonprod  34117  esplyfval2  34130  esplymhp  34133  esplyind  34140  esplyindfv  34141  esplyfvn  34142  vieta  34145  exsslsb  34162  fedgmullem1  34194  fldextrspunlsplem  34238  constrfin  34311  hashreprin  35183  reprfi2  35186  hgt750lema  35220  tgoldbachgtde  35223  kardnnfi  35762  aks4d1p4  43049  aks4d1p5  43050  aks4d1p7  43053  aks4d1p8  43057  evl1gprodd  43087  hashscontpowcl  43090  idomnnzgmulnz  43103  deg1gprod  43110  sticksstones3  43118  sticksstones22  43138  aks6d1c6lem5  43147  grpods  43164  unitscyglem1  43165  unitscyglem2  43166  unitscyglem4  43168  unitscyglem5  43169  cantnfub  44266  naddcnff  44307  fprodcnlem  46533  cnrefiisplem  46761  dvmptfprod  46877  dvnprodlem1  46878  sge0uzfsumgt  47376  hoidmvlelem1  47527  hoidmvlelem2  47528  hoidmvlelem3  47529  hoidmvlelem4  47530  hspmbllem1  47558