Theorem fssd 6602

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 6601	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
4	1, 2, 3	syl2anc 583	1 ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)

Syntax hints:   → wi 4   ⊆ wss 3883  ⟶wf 6414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-f 6422

This theorem is referenced by:  fco3OLD  6618  fconst6g  6647  fsnex  7135  tposf2  8037  mapsnd  8632  mapss  8635  ralxpmap  8642  ac6sfi  8988  infpwfien  9749  infmap2  9905  cofsmo  9956  fin23lem32  10031  axdc3lem4  10140  pwfseqlem4a  10348  fseq1p1m1  13259  seqf1olem2  13691  wrdlen2i  14583  supcvg  15496  vdwlem8  16617  isacs2  17279  funcres2b  17528  funcestrcsetclem8  17780  funcsetcestrclem8  17795  gsumress  18281  gsumwsubmcl  18390  gsumws1  18391  pj1ghm  19224  gsumval3eu  19420  gsumval3  19423  gsumsubmcl  19435  gsumzadd  19438  gsumzoppg  19460  dprdsn  19554  pwssplit1  20236  pjdm2  20828  mat1dimelbas  21528  cnrest2  22345  cnprest2  22349  1stcelcls  22520  xkoptsub  22713  tsmssubm  23202  cncfss  23968  ipcn  24315  equivcau  24369  lmcau  24382  rrx0el  24467  i1fmulclem  24772  i1fres  24775  mbfi1fseqlem4  24788  itg2mulclem  24816  limccnp  24960  dvcmulf  25014  dvcobr  25015  dvcnvlem  25045  dvcnv  25046  dvef  25049  elply2  25262  plyeq0lem  25276  plyaddlem  25281  plymullem  25282  dgrlem  25295  coeidlem  25303  jensenlem2  26042  jensen  26043  umgrupgr  27376  upgr1e  27386  umgrislfupgr  27396  usgrislfuspgr  27457  upgrres1  27583  umgrres1  27584  umgr2v2e  27795  0clwlkv  28396  minvecolem3  29139  minvecolem4  29143  occllem  29566  chscllem2  29901  chscllem4  29903  pjhf  29971  islinds5  31465  ellspds  31466  linds2eq  31477  fedgmullem1  31612  fedgmullem2  31613  locfinref  31693  esumsnf  31932  hashreprin  32500  poimirlem29  35733  dochpolN  39431  ismrc  40439  mapfzcons  40454  pwssplit4  40830  ntrf2  41623  binomcxplemnn0  41856  fcomptss  42632  fcoss  42639  frexr  42814  climreeq  43044  limccog  43051  limcrecl  43060  limsupre  43072  liminflimsupclim  43238  cncficcgt0  43319  dvdivcncf  43358  dvbdfbdioolem1  43359  ioodvbdlimc1lem1  43362  ioodvbdlimc1lem2  43363  ioodvbdlimc1  43364  ioodvbdlimc2lem  43365  ioodvbdlimc2  43366  dvnprodlem2  43378  voliooicof  43427  volicofmpt  43428  stoweidlem39  43470  stoweidlem59  43490  dirkercncflem3  43536  dirkercncf  43538  fourierdlem48  43585  fourierdlem49  43586  fourierdlem50  43587  fourierdlem51  43588  fourierdlem52  43589  fourierdlem54  43591  fourierdlem59  43596  fourierdlem70  43607  fourierdlem72  43609  fourierdlem73  43610  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem79  43616  fourierdlem84  43621  fourierdlem85  43622  fourierdlem88  43625  fourierdlem93  43630  fourierdlem94  43631  fourierdlem96  43633  fourierdlem97  43634  fourierdlem98  43635  fourierdlem99  43636  fourierdlem102  43639  fourierdlem103  43640  fourierdlem104  43641  fourierdlem111  43648  fourierdlem112  43649  fourierdlem113  43650  fourierdlem114  43651  fouriercn  43663  elaa2lem  43664  rrxtopnfi  43718  rrndistlt  43721  ioorrnopnlem  43735  issalnnd  43774  fge0icoicc  43793  fge0iccre  43802  sge0isum  43855  sge0gtfsumgt  43871  sge0seq  43874  ismeannd  43895  meaiuninclem  43908  caragenunicl  43952  caratheodorylem1  43954  caratheodorylem2  43955  isomenndlem  43958  elhoi  43970  hoicvr  43976  sge0hsphoire  44017  hoidmv1le  44022  hoiqssbllem3  44052  hspmbllem2  44055  ovolval2lem  44071  ovolval3  44075  ovolval4lem2  44078  ovolval5lem2  44081  ovolval5lem3  44082  ovnovollem1  44084  ovnovollem2  44085  iunhoiioolem  44103  iccvonmbllem  44106  vonioolem2  44109  vonioo  44110  smfco  44223  nnsum3primesgbe  45132  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  1hegrlfgr  45182  funcringcsetcALTV2lem8  45489  funcringcsetclem8ALTV  45512  mapsnop  45568  fprmappr  45569  zlmodzxzel  45579  snlindsntorlem  45699  refdivmptf  45776  refdivmptfv  45780  elbigolo1  45791  2arymaptfo  45888  prelrrx2  45947  line2  45986  line2x  45988  line2y  45989  amgmwlem  46392