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

Theorem fssd 6687
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 6686 . 2 ((𝐹:𝐴𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
41, 2, 3syl2anc 585 1 (𝜑𝐹:𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3911  wf 6493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3446  df-in 3918  df-ss 3928  df-f 6501
This theorem is referenced by:  fco3OLD  6703  fconst6g  6732  fsnex  7230  tposf2  8182  mapsnd  8827  mapss  8830  ralxpmap  8837  ac6sfi  9234  infpwfien  10003  infmap2  10159  cofsmo  10210  fin23lem32  10285  axdc3lem4  10394  pwfseqlem4a  10602  fseq1p1m1  13521  seqf1olem2  13954  wrdlen2i  14837  supcvg  15746  vdwlem8  16865  isacs2  17538  funcres2b  17788  funcestrcsetclem8  18040  funcsetcestrclem8  18055  gsumress  18542  gsumwsubmcl  18652  gsumws1  18653  pj1ghm  19490  gsumval3eu  19686  gsumval3  19689  gsumsubmcl  19701  gsumzadd  19704  gsumzoppg  19726  dprdsn  19820  pwssplit1  20535  pjdm2  21133  mat1dimelbas  21836  cnrest2  22653  cnprest2  22657  1stcelcls  22828  xkoptsub  23021  tsmssubm  23510  cncfss  24278  ipcn  24626  equivcau  24680  lmcau  24693  rrx0el  24778  i1fmulclem  25083  i1fres  25086  mbfi1fseqlem4  25099  itg2mulclem  25127  limccnp  25271  dvcmulf  25325  dvcobr  25326  dvcnvlem  25356  dvcnv  25357  dvef  25360  elply2  25573  plyeq0lem  25587  plyaddlem  25592  plymullem  25593  dgrlem  25606  coeidlem  25614  jensenlem2  26353  jensen  26354  umgrupgr  28096  upgr1e  28106  umgrislfupgr  28116  usgrislfuspgr  28177  upgrres1  28303  umgrres1  28304  umgr2v2e  28515  0clwlkv  29117  minvecolem3  29860  minvecolem4  29864  occllem  30287  chscllem2  30622  chscllem4  30624  pjhf  30692  islinds5  32203  ellspds  32204  linds2eq  32216  fedgmullem1  32381  fedgmullem2  32382  locfinref  32479  esumsnf  32720  hashreprin  33290  poimirlem29  36153  dochpolN  39999  ismrc  41067  mapfzcons  41082  pwssplit4  41459  ntrf2  42484  binomcxplemnn0  42717  fcomptss  43511  fcoss  43518  frexr  43706  climreeq  43940  limccog  43947  limcrecl  43956  limsupre  43968  liminflimsupclim  44134  cncficcgt0  44215  dvdivcncf  44254  dvbdfbdioolem1  44255  ioodvbdlimc1lem1  44258  ioodvbdlimc1lem2  44259  ioodvbdlimc1  44260  ioodvbdlimc2lem  44261  ioodvbdlimc2  44262  dvnprodlem2  44274  voliooicof  44323  volicofmpt  44324  stoweidlem39  44366  stoweidlem59  44386  dirkercncflem3  44432  dirkercncf  44434  fourierdlem48  44481  fourierdlem49  44482  fourierdlem50  44483  fourierdlem51  44484  fourierdlem52  44485  fourierdlem54  44487  fourierdlem59  44492  fourierdlem70  44503  fourierdlem72  44505  fourierdlem73  44506  fourierdlem74  44507  fourierdlem75  44508  fourierdlem76  44509  fourierdlem79  44512  fourierdlem84  44517  fourierdlem85  44518  fourierdlem88  44521  fourierdlem93  44526  fourierdlem94  44527  fourierdlem96  44529  fourierdlem97  44530  fourierdlem98  44531  fourierdlem99  44532  fourierdlem102  44535  fourierdlem103  44536  fourierdlem104  44537  fourierdlem111  44544  fourierdlem112  44545  fourierdlem113  44546  fourierdlem114  44547  fouriercn  44559  elaa2lem  44560  rrxtopnfi  44614  rrndistlt  44617  ioorrnopnlem  44631  issalnnd  44672  fge0icoicc  44692  fge0iccre  44701  sge0isum  44754  sge0gtfsumgt  44770  sge0seq  44773  ismeannd  44794  meaiuninclem  44807  caragenunicl  44851  caratheodorylem1  44853  caratheodorylem2  44854  isomenndlem  44857  elhoi  44869  hoicvr  44875  sge0hsphoire  44916  hoidmv1le  44921  hoiqssbllem3  44951  hspmbllem2  44954  ovolval2lem  44970  ovolval3  44974  ovolval4lem2  44977  ovolval5lem2  44980  ovnovollem1  44983  ovnovollem2  44984  iunhoiioolem  45002  iccvonmbllem  45005  vonioolem2  45008  vonioo  45009  smfco  45129  nnsum3primesgbe  46070  nnsum4primesodd  46074  nnsum4primesoddALTV  46075  1hegrlfgr  46120  funcringcsetcALTV2lem8  46427  funcringcsetclem8ALTV  46450  mapsnop  46506  fprmappr  46507  zlmodzxzel  46517  snlindsntorlem  46637  refdivmptf  46714  refdivmptfv  46718  elbigolo1  46729  2arymaptfo  46826  prelrrx2  46885  line2  46924  line2x  46926  line2y  46927  amgmwlem  47335
  Copyright terms: Public domain W3C validator