Theorem fssd 6687

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

Syntax hints:   → wi 4   ⊆ wss 3903  ⟶wf 6496

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3920  df-f 6504

This theorem is referenced by:  fconst6g  6731  f1ounsn  7228  fsnex  7239  tposf2  8202  mapsnd  8836  mapss  8839  ralxpmap  8846  ac6sfi  9196  infpwfien  9984  infmap2  10139  cofsmo  10191  fin23lem32  10266  axdc3lem4  10375  pwfseqlem4a  10584  fseq1p1m1  13526  seqf1olem2  13977  wrdlen2i  14877  supcvg  15791  vdwlem8  16928  isacs2  17588  funcres2b  17833  funcestrcsetclem8  18082  funcsetcestrclem8  18097  gsumress  18619  gsumwsubmcl  18774  gsumws1  18775  pj1ghm  19644  gsumval3eu  19845  gsumval3  19848  gsumsubmcl  19860  gsumzadd  19863  gsumzoppg  19885  dprdsn  19979  pwssplit1  21023  pjdm2  21678  evlsvvval  22060  psdmul  22121  mat1dimelbas  22427  cnrest2  23242  cnprest2  23246  1stcelcls  23417  xkoptsub  23610  tsmssubm  24099  cncfss  24860  ipcn  25214  equivcau  25268  lmcau  25281  rrx0el  25366  i1fmulclem  25671  i1fres  25674  mbfi1fseqlem4  25687  itg2mulclem  25715  limccnp  25860  dvcmulf  25916  dvcobr  25917  dvcobrOLD  25918  dvcnvlem  25948  dvcnv  25949  dvef  25952  elply2  26169  plyeq0lem  26183  plyaddlem  26188  plymullem  26189  dgrlem  26202  coeidlem  26210  jensenlem2  26966  jensen  26967  om2noseqlt  28307  om2noseqlt2  28308  om2noseqf1o  28309  umgrupgr  29188  upgr1e  29198  umgrislfupgr  29208  usgrislfuspgr  29272  upgrres1  29398  umgrres1  29399  umgr2v2e  29611  0clwlkv  30218  minvecolem3  30964  minvecolem4  30968  occllem  31391  chscllem2  31726  chscllem4  31728  pjhf  31796  elrgspnsubrunlem1  33341  gsumind  33438  islinds5  33460  ellspds  33461  linds2eq  33474  1arithidomlem2  33629  1arithidom  33630  dfufd2lem  33642  mplmulmvr  33716  psrmonprod  33729  mplgsum  33730  esplyfval0  33741  esplylem  33743  esplympl  33744  esplyfv1  33746  esplyfval3  33749  esplyfval1  33750  esplyfvaln  33751  esplyind  33752  fedgmullem1  33807  fedgmullem2  33808  locfinref  34019  esumsnf  34242  hashreprin  34798  poimirlem29  37900  dochpolN  41866  aks6d1c7lem1  42550  evlsbagval  42927  evlsmhpvvval  42953  mhphf  42955  ismrc  43058  mapfzcons  43073  pwssplit4  43446  ntrf2  44480  binomcxplemnn0  44705  fcomptss  45561  fcoss  45568  frexr  45743  climreeq  45973  limccog  45980  limcrecl  45989  limsupre  45999  liminflimsupclim  46165  cncficcgt0  46246  dvdivcncf  46285  dvbdfbdioolem1  46286  ioodvbdlimc1lem1  46289  ioodvbdlimc1lem2  46290  ioodvbdlimc1  46291  ioodvbdlimc2lem  46292  ioodvbdlimc2  46293  dvnprodlem2  46305  voliooicof  46354  volicofmpt  46355  stoweidlem39  46397  stoweidlem59  46417  dirkercncflem3  46463  dirkercncf  46465  fourierdlem48  46512  fourierdlem49  46513  fourierdlem50  46514  fourierdlem51  46515  fourierdlem52  46516  fourierdlem54  46518  fourierdlem59  46523  fourierdlem70  46534  fourierdlem72  46536  fourierdlem73  46537  fourierdlem74  46538  fourierdlem75  46539  fourierdlem76  46540  fourierdlem79  46543  fourierdlem84  46548  fourierdlem85  46549  fourierdlem88  46552  fourierdlem93  46557  fourierdlem94  46558  fourierdlem96  46560  fourierdlem97  46561  fourierdlem98  46562  fourierdlem99  46563  fourierdlem102  46566  fourierdlem103  46567  fourierdlem104  46568  fourierdlem111  46575  fourierdlem112  46576  fourierdlem113  46577  fourierdlem114  46578  fouriercn  46590  elaa2lem  46591  rrxtopnfi  46645  rrndistlt  46648  ioorrnopnlem  46662  issalnnd  46703  fge0icoicc  46723  fge0iccre  46732  sge0isum  46785  sge0gtfsumgt  46801  sge0seq  46804  ismeannd  46825  meaiuninclem  46838  caragenunicl  46882  caratheodorylem1  46884  caratheodorylem2  46885  isomenndlem  46888  elhoi  46900  hoicvr  46906  sge0hsphoire  46947  hoidmv1le  46952  hoiqssbllem3  46982  hspmbllem2  46985  ovolval2lem  47001  ovolval3  47005  ovolval4lem2  47008  ovolval5lem2  47011  ovnovollem1  47014  ovnovollem2  47015  iunhoiioolem  47033  iccvonmbllem  47036  vonioolem2  47039  vonioo  47040  smfco  47160  nnsum3primesgbe  48152  nnsum4primesodd  48156  nnsum4primesoddALTV  48157  grimuhgr  48247  uhgrimisgrgric  48291  isubgr3stgrlem6  48331  1hegrlfgr  48492  funcringcsetcALTV2lem8  48657  funcringcsetclem8ALTV  48680  mapsnop  48704  fprmappr  48705  zlmodzxzel  48715  snlindsntorlem  48830  refdivmptf  48902  refdivmptfv  48906  elbigolo1  48917  2arymaptfo  49014  prelrrx2  49073  line2  49112  line2x  49114  line2y  49115  amgmwlem  50161