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

Theorem fssd 6521
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 6520 . 2 ((𝐹:𝐴𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
41, 2, 3syl2anc 584 1 (𝜑𝐹:𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3933  wf 6344
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-in 3940  df-ss 3949  df-f 6352
This theorem is referenced by:  fconst6g  6561  fsnex  7030  tposf2  7905  mapsnd  8438  mapss  8441  ralxpmap  8448  ac6sfi  8750  infpwfien  9476  infmap2  9628  cofsmo  9679  fin23lem32  9754  axdc3lem4  9863  pwfseqlem4a  10071  fseq1p1m1  12969  seqf1olem2  13398  wrdlen2i  14292  supcvg  15199  vdwlem8  16312  isacs2  16912  funcres2b  17155  funcestrcsetclem8  17385  funcsetcestrclem8  17400  gsumress  17880  gsumwsubmcl  17989  gsumws1  17990  pj1ghm  18758  gsumval3eu  18953  gsumval3  18956  gsumsubmcl  18968  gsumzadd  18971  gsumzoppg  18993  dprdsn  19087  pwssplit1  19760  pjdm2  20783  mat1dimelbas  21008  cnrest2  21822  cnprest2  21826  1stcelcls  21997  xkoptsub  22190  tsmssubm  22678  cncfss  23434  ipcn  23776  equivcau  23830  lmcau  23843  rrx0el  23928  i1fmulclem  24230  i1fres  24233  mbfi1fseqlem4  24246  itg2mulclem  24274  limccnp  24416  dvcmulf  24469  dvcobr  24470  dvcnvlem  24500  dvcnv  24501  dvef  24504  elply2  24713  plyeq0lem  24727  plyaddlem  24732  plymullem  24733  dgrlem  24746  coeidlem  24754  jensenlem2  25492  jensen  25493  umgrupgr  26815  upgr1e  26825  umgrislfupgr  26835  usgrislfuspgr  26896  upgrres1  27022  umgrres1  27023  umgr2v2e  27234  0clwlkv  27837  minvecolem3  28580  minvecolem4  28584  occllem  29007  chscllem2  29342  chscllem4  29344  pjhf  29412  islinds5  30859  ellspds  30860  linds2eq  30868  fedgmullem1  30924  fedgmullem2  30925  locfinref  31004  esumsnf  31222  hashreprin  31790  poimirlem29  34802  dochpolN  38506  ismrc  39176  mapfzcons  39191  pwssplit4  39567  ntrf2  40352  binomcxplemnn0  40558  fcomptss  41342  fcoss  41349  fco3  41367  frexr  41531  climreeq  41770  limccog  41777  limcrecl  41786  limsupre  41798  liminflimsupclim  41964  cncficcgt0  42047  dvdivcncf  42088  dvbdfbdioolem1  42089  ioodvbdlimc1lem1  42092  ioodvbdlimc1lem2  42093  ioodvbdlimc1  42094  ioodvbdlimc2lem  42095  ioodvbdlimc2  42096  dvnprodlem2  42108  voliooicof  42158  volicofmpt  42159  stoweidlem39  42201  stoweidlem59  42221  dirkercncflem3  42267  dirkercncf  42269  fourierdlem48  42316  fourierdlem49  42317  fourierdlem50  42318  fourierdlem51  42319  fourierdlem52  42320  fourierdlem54  42322  fourierdlem59  42327  fourierdlem70  42338  fourierdlem72  42340  fourierdlem73  42341  fourierdlem74  42342  fourierdlem75  42343  fourierdlem76  42344  fourierdlem79  42347  fourierdlem84  42352  fourierdlem85  42353  fourierdlem88  42356  fourierdlem93  42361  fourierdlem94  42362  fourierdlem96  42364  fourierdlem97  42365  fourierdlem98  42366  fourierdlem99  42367  fourierdlem102  42370  fourierdlem103  42371  fourierdlem104  42372  fourierdlem111  42379  fourierdlem112  42380  fourierdlem113  42381  fourierdlem114  42382  fouriercn  42394  elaa2lem  42395  rrxtopnfi  42449  rrndistlt  42452  ioorrnopnlem  42466  issalnnd  42505  fge0icoicc  42524  fge0iccre  42533  sge0isum  42586  sge0gtfsumgt  42602  sge0seq  42605  ismeannd  42626  meaiuninclem  42639  caragenunicl  42683  caratheodorylem1  42685  caratheodorylem2  42686  isomenndlem  42689  elhoi  42701  hoicvr  42707  sge0hsphoire  42748  hoidmv1le  42753  hoiqssbllem3  42783  hspmbllem2  42786  ovolval2lem  42802  ovolval3  42806  ovolval4lem2  42809  ovolval5lem2  42812  ovolval5lem3  42813  ovnovollem1  42815  ovnovollem2  42816  iunhoiioolem  42834  iccvonmbllem  42837  vonioolem2  42840  vonioo  42841  smfco  42954  nnsum3primesgbe  43834  nnsum4primesodd  43838  nnsum4primesoddALTV  43839  1hegrlfgr  43884  funcringcsetcALTV2lem8  44242  funcringcsetclem8ALTV  44265  mapsnop  44321  mapprop  44322  zlmodzxzel  44331  snlindsntorlem  44453  refdivmptf  44530  refdivmptfv  44534  elbigolo1  44545  prelrrx2  44628  line2  44667  line2x  44669  line2y  44670  amgmwlem  44831
  Copyright terms: Public domain W3C validator