MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssfid Structured version   Visualization version   GIF version

Theorem ssfid 9208
Description: A subset of a finite set is finite, deduction version of ssfi 9114. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
Hypotheses
Ref Expression
ssfid.1 (𝜑𝐴 ∈ Fin)
ssfid.2 (𝜑𝐵𝐴)
Assertion
Ref Expression
ssfid (𝜑𝐵 ∈ Fin)

Proof of Theorem ssfid
StepHypRef Expression
1 ssfid.1 . 2 (𝜑𝐴 ∈ Fin)
2 ssfid.2 . 2 (𝜑𝐵𝐴)
3 ssfi 9114 . 2 ((𝐴 ∈ Fin ∧ 𝐵𝐴) → 𝐵 ∈ Fin)
41, 2, 3syl2anc 584 1 (𝜑𝐵 ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  wss 3909  Fincfn 8880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5255  ax-nul 5262  ax-pr 5383  ax-un 7669
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2888  df-ne 2943  df-ral 3064  df-rex 3073  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-br 5105  df-opab 5167  df-tr 5222  df-id 5530  df-eprel 5536  df-po 5544  df-so 5545  df-fr 5587  df-we 5589  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-ord 6319  df-on 6320  df-lim 6321  df-suc 6322  df-iota 6446  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-om 7800  df-1o 8409  df-en 8881  df-fin 8884
This theorem is referenced by:  ixpfi  9290  fisuppfi  9310  fsuppunbi  9323  ressuppfi  9328  fsuppmptif  9332  fsuppco2  9336  fsuppcor  9337  marypha1lem  9366  wemapso2lem  9485  cantnfp1lem1  9611  pwfseqlem4  10595  hashbclem  14346  hashf1lem2  14352  phphashd  14362  isercolllem2  15547  isercoll  15549  fsum2dlem  15652  fsumcom2  15656  fsumless  15678  fsumabs  15683  fsumrlim  15693  fsumo1  15694  fsumiun  15703  qshash  15709  incexc  15719  incexc2  15720  fprod2dlem  15860  fprodcom2  15864  4sqlem11  16824  vdwlem11  16860  ramlb  16888  0ram  16889  ramub1lem1  16895  ramub1lem2  16896  prmgaplem4  16923  isstruct2  17018  lagsubg2  18987  lagsubg  18988  orbsta2  19090  symgbasfi  19156  oddvds2  19344  sylow1lem3  19378  sylow1lem4  19379  sylow1lem5  19380  odcau  19382  pgpssslw  19392  sylow2alem2  19396  sylow2a  19397  sylow2blem1  19398  sylow2blem3  19400  slwhash  19402  fislw  19403  sylow2  19404  sylow3lem1  19405  sylow3lem3  19407  sylow3lem4  19408  sylow3lem6  19410  cyggenod  19657  gsumval3lem2  19679  gsumzadd  19695  gsum2dlem1  19743  gsum2dlem2  19744  gsum2d  19745  gsum2d2lem  19746  dprdfadd  19795  ablfac1eu  19848  pgpfac1lem5  19854  pgpfaclem2  19857  pgpfaclem3  19858  ablfaclem3  19862  prmgrpsimpgd  19889  lcomfsupp  20358  dsmmacl  21143  dsmmsubg  21145  dsmmlss  21146  frlmsslsp  21198  psrbaglecl  21324  psrbagleclOLD  21325  psrbagaddcl  21326  psrbagaddclOLD  21327  psrbagcon  21328  psrbagconOLD  21329  mplcoe5  21437  mhpmulcl  21535  mamures  21735  mdetrlin  21947  mdetrsca  21948  mdetralt  21953  madugsum  21988  fin1aufil  23279  xrge0gsumle  24192  xrge0tsms  24193  fsumcn  24229  rrxcph  24752  rrxmval  24765  i1fadd  25055  i1fmul  25056  i1fmulc  25064  i1fres  25066  mbfi1fseqlem4  25079  itgfsum  25187  dvmptfsum  25335  jensenlem1  26332  jensenlem2  26333  jensen  26334  0sgm  26489  sgmf  26490  sgmnncl  26492  fsumdvdsdiag  26529  fsumdvdscom  26530  dvdsflsumcom  26533  musum  26536  musumsum  26537  muinv  26538  fsumdvdsmul  26540  vmasum  26560  perfectlem2  26574  dchrfi  26599  rplogsumlem2  26829  rpvmasumlem  26831  dchrvmasumlem1  26839  dchrisum0ff  26851  dchrisum0  26864  vmalogdivsum2  26882  logsqvma  26886  logsqvma2  26887  selberg  26892  selberg34r  26915  pntsval2  26920  pntrlog2bndlem1  26921  wwlksnfi  28749  wspthnfi  28762  wspthnonfi  28765  clwwlknfi  28887  qerclwwlknfi  28915  clwlknon2num  29210  numclwlk1lem2  29212  fsuppinisegfi  31498  offinsupp1  31539  fsumiunle  31620  elrspunidl  32094  fedgmullem1  32215  hashreprin  33124  reprfi2  33127  hgt750lema  33161  tgoldbachgtde  33164  aks4d1p4  40525  aks4d1p5  40526  aks4d1p7  40529  aks4d1p8  40533  sticksstones3  40545  sticksstones22  40565  evlsbagval  40726  mhphf  40747  cantnfub  41631  naddcnff  41652  finnzfsuppd  42462  fprodcnlem  43810  cnrefiisplem  44040  sge0uzfsumgt  44655  hoidmvlelem1  44806  hoidmvlelem2  44807  hoidmvlelem3  44808  hoidmvlelem4  44809  hspmbllem1  44837
  Copyright terms: Public domain W3C validator