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

Theorem fssd 6095
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 6094 . 2 ((𝐹:𝐴𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
41, 2, 3syl2anc 694 1 (𝜑𝐹:𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3607  wf 5922
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621  df-f 5930
This theorem is referenced by:  fconst6g  6132  tposf2  7421  mapss  7942  ralxpmap  7949  ac6sfi  8245  infpwfien  8923  infmap2  9078  cofsmo  9129  fin23lem32  9204  axdc3lem4  9313  pwfseqlem4a  9521  fseq1p1m1  12452  seqf1olem2  12881  wrdlen2i  13732  supcvg  14632  vdwlem8  15739  isacs2  16361  funcres2b  16604  funcestrcsetclem8  16834  funcsetcestrclem8  16849  gsumress  17323  gsumwsubmcl  17422  gsumws1  17423  pj1ghm  18162  gsumval3eu  18351  gsumval3  18354  gsumsubmcl  18365  gsumzadd  18368  gsumzoppg  18390  dprdsn  18481  pwssplit1  19107  pjdm2  20103  mat1dimelbas  20325  cnrest2  21138  cnprest2  21142  1stcelcls  21312  xkoptsub  21505  tsmssubm  21993  cncfss  22749  ipcn  23091  equivcau  23144  lmcau  23157  i1fmulclem  23514  i1fres  23517  mbfi1fseqlem4  23530  itg2mulclem  23558  limccnp  23700  dvcmulf  23753  dvcobr  23754  dvcnvlem  23784  dvcnv  23785  dvef  23788  elply2  23997  plyeq0lem  24011  plyaddlem  24016  plymullem  24017  dgrlem  24030  coeidlem  24038  jensenlem2  24759  jensen  24760  umgrupgr  26043  upgr1e  26053  umgrislfupgr  26063  usgrislfuspgr  26124  upgrres1  26250  umgrres1  26251  umgr2v2e  26477  0clwlkv  27109  minvecolem3  27860  minvecolem4  27864  occllem  28290  chscllem2  28625  chscllem4  28627  pjhf  28695  locfinref  30036  esumsnf  30254  hashreprin  30826  poimirlem29  33568  dochpolN  37096  ismrc  37581  mapfzcons  37596  pwssplit4  37976  ntrf2  38739  binomcxplemnn0  38865  fcomptss  39709  fcoss  39716  fco3  39735  frexr  39917  climreeq  40163  limccog  40170  limcrecl  40179  limsupre  40191  liminflimsupclim  40357  cncficcgt0  40419  dvdivcncf  40460  dvbdfbdioolem1  40461  ioodvbdlimc1lem1  40464  ioodvbdlimc1lem2  40465  ioodvbdlimc1  40466  ioodvbdlimc2lem  40467  ioodvbdlimc2  40468  dvnprodlem2  40480  voliooicof  40531  volicofmpt  40532  stoweidlem39  40574  stoweidlem59  40594  dirkercncflem3  40640  dirkercncf  40642  fourierdlem48  40689  fourierdlem49  40690  fourierdlem50  40691  fourierdlem51  40692  fourierdlem52  40693  fourierdlem54  40695  fourierdlem59  40700  fourierdlem70  40711  fourierdlem72  40713  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem76  40717  fourierdlem79  40720  fourierdlem84  40725  fourierdlem85  40726  fourierdlem88  40729  fourierdlem93  40734  fourierdlem94  40735  fourierdlem96  40737  fourierdlem97  40738  fourierdlem98  40739  fourierdlem99  40740  fourierdlem102  40743  fourierdlem103  40744  fourierdlem104  40745  fourierdlem111  40752  fourierdlem112  40753  fourierdlem113  40754  fourierdlem114  40755  fouriercn  40767  elaa2lem  40768  rrxtopnfi  40824  rrndistlt  40828  ioorrnopnlem  40842  issalnnd  40881  fge0icoicc  40900  fge0iccre  40909  sge0isum  40962  sge0gtfsumgt  40978  sge0seq  40981  ismeannd  41002  meaiuninclem  41015  caragenunicl  41059  caratheodorylem1  41061  caratheodorylem2  41062  isomenndlem  41065  elhoi  41077  hoicvr  41083  sge0hsphoire  41124  hoidmv1le  41129  hoiqssbllem3  41159  hspmbllem2  41162  ovolval2lem  41178  ovolval3  41182  ovolval4lem2  41185  ovolval5lem2  41188  ovolval5lem3  41189  ovnovollem1  41191  ovnovollem2  41192  iunhoiioolem  41210  iccvonmbllem  41213  vonioolem2  41216  vonioo  41217  smfco  41330  nnsum3primesgbe  42005  nnsum4primesodd  42009  nnsum4primesoddALTV  42010  1hegrlfgr  42038  funcringcsetcALTV2lem8  42368  funcringcsetclem8ALTV  42391  mapsnop  42448  mapprop  42449  zlmodzxzel  42458  snlindsntorlem  42584  refdivmptf  42661  refdivmptfv  42665  elbigolo1  42676  amgmwlem  42876
  Copyright terms: Public domain W3C validator