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

Theorem fssd 5970
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 5969 . 2 ((𝐹:𝐴𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
41, 2, 3syl2anc 691 1 (𝜑𝐹:𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3540  wf 5800
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 5808
This theorem is referenced by:  fconst6g  6007  tposf2  7263  mapss  7786  ralxpmap  7793  ac6sfi  8089  infpwfien  8768  infmap2  8923  cofsmo  8974  fin23lem32  9049  axdc3lem4  9158  pwfseqlem4a  9362  fseq1p1m1  12283  seqf1olem2  12703  wrdlen2i  13534  supcvg  14427  vdwlem8  15530  isacs2  16137  funcres2b  16380  funcestrcsetclem8  16610  funcsetcestrclem8  16625  gsumress  17099  gsumwsubmcl  17198  gsumws1  17199  pj1ghm  17939  gsumval3eu  18128  gsumval3  18131  gsumsubmcl  18142  gsumzadd  18145  gsumzoppg  18167  dprdsn  18258  pwssplit1  18880  pjdm2  19874  mat1dimelbas  20096  cnrest2  20900  cnprest2  20904  1stcelcls  21074  xkoptsub  21267  tsmssubm  21756  cncfss  22510  ipcn  22853  equivcau  22906  lmcau  22919  i1fmulclem  23275  i1fres  23278  mbfi1fseqlem4  23291  itg2mulclem  23319  limccnp  23461  dvcmulf  23514  dvcobr  23515  dvcnvlem  23543  dvcnv  23544  dvef  23547  elply2  23756  plyeq0lem  23770  plyaddlem  23775  plymullem  23776  dgrlem  23789  coeidlem  23797  jensenlem2  24514  jensen  24515  umgrupgr  25769  upgr1e  25779  umgrislfupgr  25789  umgra1  25855  2trllemH  26082  constr1trl  26118  constr3trllem3  26180  eupa0  26501  eupap1  26503  minvecolem3  27116  minvecolem4  27120  occllem  27546  chscllem2  27881  chscllem4  27883  pjhf  27951  locfinref  29236  esumsnf  29453  poimirlem29  32608  dochpolN  35797  ismrc  36282  mapfzcons  36297  pwssplit4  36677  ntrf2  37442  binomcxplemnn0  37570  fcomptss  38390  fcoss  38397  fco3  38416  frexr  38545  climreeq  38680  limccog  38687  limcrecl  38696  limsupre  38708  cncficcgt0  38774  dvdivcncf  38817  dvbdfbdioolem1  38818  ioodvbdlimc1lem1  38821  ioodvbdlimc1lem2  38822  ioodvbdlimc1  38823  ioodvbdlimc2lem  38824  ioodvbdlimc2  38825  dvnprodlem2  38837  voliooicof  38889  volicofmpt  38890  stoweidlem39  38932  stoweidlem59  38952  dirkercncflem3  38998  dirkercncf  39000  fourierdlem48  39047  fourierdlem49  39048  fourierdlem50  39049  fourierdlem51  39050  fourierdlem52  39051  fourierdlem54  39053  fourierdlem59  39058  fourierdlem70  39069  fourierdlem72  39071  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem79  39078  fourierdlem84  39083  fourierdlem85  39084  fourierdlem88  39087  fourierdlem93  39092  fourierdlem94  39093  fourierdlem96  39095  fourierdlem97  39096  fourierdlem98  39097  fourierdlem99  39098  fourierdlem102  39101  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  fourierdlem112  39111  fourierdlem113  39112  fourierdlem114  39113  fouriercn  39125  elaa2lem  39126  rrxtopnfi  39182  rrndistlt  39186  ioorrnopnlem  39200  issalnnd  39239  fge0icoicc  39258  fge0iccre  39267  sge0isum  39320  sge0gtfsumgt  39336  sge0seq  39339  ismeannd  39360  meaiuninclem  39373  caragenunicl  39414  caratheodorylem1  39416  caratheodorylem2  39417  isomenndlem  39420  elhoi  39432  hoicvr  39438  sge0hsphoire  39479  hoidmv1le  39484  hoiqssbllem3  39514  hspmbllem2  39517  ovolval2lem  39533  ovolval3  39537  ovolval4lem2  39540  ovolval5lem2  39543  ovolval5lem3  39544  ovnovollem1  39546  ovnovollem2  39547  iunhoiioolem  39566  iccvonmbllem  39569  vonioolem2  39572  vonioo  39573  smfco  39687  nnsum3primesgbe  40208  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  usgrislfuspgr  40414  upgrres1  40532  umgrres1  40533  1hegrlfgr  40722  umgr2v2e  40741  funcringcsetcALTV2lem8  41835  funcringcsetclem8ALTV  41858  mapsnop  41916  mapprop  41917  zlmodzxzel  41926  snlindsntorlem  42053  refdivmptf  42134  refdivmptfv  42138  elbigolo1  42149  amgmwlem  42357
  Copyright terms: Public domain W3C validator