Theorem fssd 6709

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

Step	Hyp	Ref	Expression
1		fssd.f	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		fssd.b	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
3		fss 6708	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
4	1, 2, 3	syl2anc 593	1 ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)

Syntax hints:   → wi 4   ⊆ wss 3904  ⟶wf 6517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829

This theorem depends on definitions:  df-bi 209  df-an 400  df-ss 3921  df-f 6525

This theorem is referenced by:  fconst6g  6753  f1ounsn  7256  fsnex  7267  tposf2  8230  mapsnd  8868  mapss  8871  ralxpmap  8878  ac6sfi  9228  infpwfien  10018  infmap2  10173  cofsmo  10226  fin23lem32  10301  axdc3lem4  10410  pwfseqlem4a  10619  fseq1p1m1  13603  seqf1olem2  14055  wrdlen2i  14955  supcvg  15886  vdwlem8  17024  isacs2  17685  funcres2b  17930  funcestrcsetclem8  18179  funcsetcestrclem8  18194  gsumress  18716  gsumwsubmcl  18871  gsumws1  18872  pj1ghm  19743  gsumval3eu  19944  gsumval3  19947  gsumsubmcl  19959  gsumzadd  19962  gsumzoppg  19984  dprdsn  20078  pwssplit1  21123  pjdm2  21760  evlsvvval  22143  psdmul  22228  mat1dimelbas  22528  cnrest2  23343  cnprest2  23347  1stcelcls  23518  xkoptsub  23711  tsmssubm  24200  cncfss  24958  ipcn  25305  equivcau  25359  lmcau  25372  rrx0el  25457  i1fmulclem  25761  i1fres  25764  mbfi1fseqlem4  25777  itg2mulclem  25805  limccnp  25950  dvcmulf  26004  dvcobr  26005  dvcnvlem  26035  dvcnv  26036  dvef  26039  elply2  26253  plyeq0lem  26267  plyaddlem  26272  plymullem  26273  dgrlem  26286  coeidlem  26294  jensenlem2  27049  jensen  27050  om2noseqlt  28389  om2noseqlt2  28390  om2noseqf1o  28391  umgrupgr  29301  upgr1e  29311  umgrislfupgr  29321  usgrislfuspgr  29385  upgrres1  29511  umgrres1  29512  umgr2v2e  29723  0clwlkv  30330  minvecolem3  31076  minvecolem4  31080  occllem  31503  chscllem2  31838  chscllem4  31840  pjhf  31908  elrgspnsubrunlem1  33425  gsumind  33528  islinds5  33550  ellspds  33551  linds2eq  33564  1arithidomlem2  33729  1arithidom  33730  dfufd2lem  33742  selvply1rhmlemb  33813  mplmulmvr  33833  psrmonprod  33846  mplgsum  33847  esplyfval0  33858  esplylem  33860  esplympl  33861  esplyfv1  33863  esplyfval3  33866  esplyfval1  33867  esplyfvaln  33868  esplyind  33869  fedgmullem1  33923  fedgmullem2  33924  locfinref  34135  esumsnf  34358  hashreprin  34911  poimirlem29  38145  dochpolN  42111  aks6d1c7lem1  42794  evlsbagval  43165  evlsmhpvvval  43174  mhphf  43176  ismrc  43279  mapfzcons  43294  pwssplit4  43663  ntrf2  44697  binomcxplemnn0  44922  fcomptss  45777  fcoss  45783  frexr  45957  climreeq  46186  limccog  46193  limcrecl  46202  limsupre  46212  liminflimsupclim  46378  cncficcgt0  46459  dvdivcncf  46498  dvbdfbdioolem1  46499  ioodvbdlimc1lem1  46502  ioodvbdlimc1lem2  46503  ioodvbdlimc1  46504  ioodvbdlimc2lem  46505  ioodvbdlimc2  46506  dvnprodlem2  46518  voliooicof  46567  volicofmpt  46568  stoweidlem39  46610  stoweidlem59  46630  dirkercncflem3  46676  dirkercncf  46678  fourierdlem48  46725  fourierdlem49  46726  fourierdlem50  46727  fourierdlem51  46728  fourierdlem52  46729  fourierdlem54  46731  fourierdlem59  46736  fourierdlem70  46747  fourierdlem72  46749  fourierdlem73  46750  fourierdlem74  46751  fourierdlem75  46752  fourierdlem76  46753  fourierdlem79  46756  fourierdlem84  46761  fourierdlem85  46762  fourierdlem88  46765  fourierdlem93  46770  fourierdlem94  46771  fourierdlem96  46773  fourierdlem97  46774  fourierdlem98  46775  fourierdlem99  46776  fourierdlem102  46779  fourierdlem103  46780  fourierdlem104  46781  fourierdlem111  46788  fourierdlem112  46789  fourierdlem113  46790  fourierdlem114  46791  fouriercn  46803  elaa2lem  46804  rrxtopnfi  46858  rrndistlt  46861  ioorrnopnlem  46875  issalnnd  46916  fge0icoicc  46936  fge0iccre  46945  sge0isum  46998  sge0gtfsumgt  47014  sge0seq  47017  ismeannd  47038  meaiuninclem  47051  caragenunicl  47095  caratheodorylem1  47097  caratheodorylem2  47098  isomenndlem  47101  elhoi  47113  sge0hsphoire  47160  hoidmv1le  47165  hoiqssbllem3  47195  hspmbllem2  47198  ovolval2lem  47214  ovolval3  47218  ovolval4lem2  47221  ovolval5lem2  47224  ovnovollem1  47227  ovnovollem2  47228  iunhoiioolem  47246  iccvonmbllem  47249  vonioolem2  47252  vonioo  47253  smfco  47373  nnsum3primesgbe  48411  nnsum4primesodd  48415  nnsum4primesoddALTV  48416  grimuhgr  48506  uhgrimisgrgric  48550  isubgr3stgrlem6  48590  1hegrlfgr  48751  funcringcsetcALTV2lem8  48916  funcringcsetclem8ALTV  48939  mapsnop  48963  fprmappr  48964  zlmodzxzel  48974  snlindsntorlem  49089  refdivmptf  49161  refdivmptfv  49165  elbigolo1  49176  2arymaptfo  49273  prelrrx2  49332  line2  49371  line2x  49373  line2y  49374  amgmwlem  50420