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

Theorem fssd 5956
Description: Expanding the codomain of a mapping, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fssd.f (𝜑𝐹:𝐴𝐵)
fssd.b (𝜑𝐵𝐶)
Assertion
Ref Expression
fssd (𝜑𝐹:𝐴𝐶)

Proof of Theorem fssd
StepHypRef Expression
1 fssd.f . 2 (𝜑𝐹:𝐴𝐵)
2 fssd.b . 2 (𝜑𝐵𝐶)
3 fss 5955 . 2 ((𝐹:𝐴𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
41, 2, 3syl2anc 691 1 (𝜑𝐹:𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3540  wf 5786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554  df-f 5794
This theorem is referenced by:  fconst6g  5992  tposf2  7241  mapss  7764  ralxpmap  7771  ac6sfi  8067  infpwfien  8746  infmap2  8901  cofsmo  8952  fin23lem32  9027  axdc3lem4  9136  pwfseqlem4a  9340  fseq1p1m1  12241  seqf1olem2  12661  wrdlen2i  13483  supcvg  14376  vdwlem8  15479  isacs2  16086  funcres2b  16329  funcestrcsetclem8  16559  funcsetcestrclem8  16574  gsumress  17048  gsumwsubmcl  17147  gsumws1  17148  pj1ghm  17888  gsumval3eu  18077  gsumval3  18080  gsumsubmcl  18091  gsumzadd  18094  gsumzoppg  18116  dprdsn  18207  pwssplit1  18829  pjdm2  19822  mat1dimelbas  20044  cnrest2  20848  cnprest2  20852  1stcelcls  21022  xkoptsub  21215  tsmssubm  21704  cncfss  22458  ipcn  22798  equivcau  22851  lmcau  22864  i1fmulclem  23220  i1fres  23223  mbfi1fseqlem4  23236  itg2mulclem  23264  limccnp  23406  dvcmulf  23459  dvcobr  23460  dvcnvlem  23488  dvcnv  23489  dvef  23492  elply2  23701  plyeq0lem  23715  plyaddlem  23720  plymullem  23721  dgrlem  23734  coeidlem  23742  jensenlem2  24459  jensen  24460  umgra1  25649  2trllemH  25876  constr1trl  25912  constr3trllem3  25974  eupa0  26295  eupap1  26297  minvecolem3  26910  minvecolem4  26914  occllem  27340  chscllem2  27675  chscllem4  27677  pjhf  27745  locfinref  29030  esumsnf  29247  poimirlem29  32402  dochpolN  35591  ismrc  36076  mapfzcons  36091  pwssplit4  36471  ntrf2  37236  binomcxplemnn0  37364  fcomptss  38184  fcoss  38191  fco3  38210  frexr  38339  climreeq  38474  limccog  38481  limcrecl  38490  limsupre  38502  cncficcgt0  38568  dvdivcncf  38611  dvbdfbdioolem1  38612  ioodvbdlimc1lem1  38615  ioodvbdlimc1lem2  38616  ioodvbdlimc1  38617  ioodvbdlimc2lem  38618  ioodvbdlimc2  38619  dvnprodlem2  38631  voliooicof  38683  volicofmpt  38684  stoweidlem39  38726  stoweidlem59  38746  dirkercncflem3  38792  dirkercncf  38794  fourierdlem48  38841  fourierdlem49  38842  fourierdlem50  38843  fourierdlem51  38844  fourierdlem52  38845  fourierdlem54  38847  fourierdlem59  38852  fourierdlem70  38863  fourierdlem72  38865  fourierdlem73  38866  fourierdlem74  38867  fourierdlem75  38868  fourierdlem76  38869  fourierdlem79  38872  fourierdlem84  38877  fourierdlem85  38878  fourierdlem88  38881  fourierdlem93  38886  fourierdlem94  38887  fourierdlem96  38889  fourierdlem97  38890  fourierdlem98  38891  fourierdlem99  38892  fourierdlem102  38895  fourierdlem103  38896  fourierdlem104  38897  fourierdlem111  38904  fourierdlem112  38905  fourierdlem113  38906  fourierdlem114  38907  fouriercn  38919  elaa2lem  38920  rrxtopnfi  38976  rrndistlt  38980  ioorrnopnlem  38994  issalnnd  39033  fge0icoicc  39052  fge0iccre  39061  sge0isum  39114  sge0gtfsumgt  39130  sge0seq  39133  ismeannd  39154  meaiuninclem  39167  caragenunicl  39208  caratheodorylem1  39210  caratheodorylem2  39211  isomenndlem  39214  elhoi  39226  hoicvr  39232  sge0hsphoire  39273  hoidmv1le  39278  hoiqssbllem3  39308  hspmbllem2  39311  ovolval2lem  39327  ovolval3  39331  ovolval4lem2  39334  ovolval5lem2  39337  ovolval5lem3  39338  ovnovollem1  39340  ovnovollem2  39341  iunhoiioolem  39360  iccvonmbllem  39363  vonioolem2  39366  vonioo  39367  smfco  39481  nnsum3primesgbe  40003  nnsum4primesodd  40007  nnsum4primesoddALTV  40008  umgrupgr  40320  upgr1e  40330  umgrislfupgr  40340  usgrislfuspgr  40406  upgrres1  40524  umgrres1  40525  1hegrlfgr  40714  umgr2v2e  40733  funcringcsetcALTV2lem8  41827  funcringcsetclem8ALTV  41850  mapsnop  41908  mapprop  41909  zlmodzxzel  41918  snlindsntorlem  42045  refdivmptf  42126  refdivmptfv  42130  elbigolo1  42141  amgmwlem  42310
  Copyright terms: Public domain W3C validator