Theorem fssd 6679

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

Syntax hints:   → wi 4   ⊆ wss 3901  ⟶wf 6488

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3918  df-f 6496

This theorem is referenced by:  fconst6g  6723  f1ounsn  7218  fsnex  7229  tposf2  8192  mapsnd  8824  mapss  8827  ralxpmap  8834  ac6sfi  9184  infpwfien  9972  infmap2  10127  cofsmo  10179  fin23lem32  10254  axdc3lem4  10363  pwfseqlem4a  10572  fseq1p1m1  13514  seqf1olem2  13965  wrdlen2i  14865  supcvg  15779  vdwlem8  16916  isacs2  17576  funcres2b  17821  funcestrcsetclem8  18070  funcsetcestrclem8  18085  gsumress  18607  gsumwsubmcl  18762  gsumws1  18763  pj1ghm  19632  gsumval3eu  19833  gsumval3  19836  gsumsubmcl  19848  gsumzadd  19851  gsumzoppg  19873  dprdsn  19967  pwssplit1  21011  pjdm2  21666  evlsvvval  22048  psdmul  22109  mat1dimelbas  22415  cnrest2  23230  cnprest2  23234  1stcelcls  23405  xkoptsub  23598  tsmssubm  24087  cncfss  24848  ipcn  25202  equivcau  25256  lmcau  25269  rrx0el  25354  i1fmulclem  25659  i1fres  25662  mbfi1fseqlem4  25675  itg2mulclem  25703  limccnp  25848  dvcmulf  25904  dvcobr  25905  dvcobrOLD  25906  dvcnvlem  25936  dvcnv  25937  dvef  25940  elply2  26157  plyeq0lem  26171  plyaddlem  26176  plymullem  26177  dgrlem  26190  coeidlem  26198  jensenlem2  26954  jensen  26955  om2noseqlt  28295  om2noseqlt2  28296  om2noseqf1o  28297  umgrupgr  29176  upgr1e  29186  umgrislfupgr  29196  usgrislfuspgr  29260  upgrres1  29386  umgrres1  29387  umgr2v2e  29599  0clwlkv  30206  minvecolem3  30951  minvecolem4  30955  occllem  31378  chscllem2  31713  chscllem4  31715  pjhf  31783  elrgspnsubrunlem1  33329  gsumind  33426  islinds5  33448  ellspds  33449  linds2eq  33462  1arithidomlem2  33617  1arithidom  33618  dfufd2lem  33630  mplmulmvr  33704  esplyfval0  33722  esplylem  33724  esplympl  33725  esplyfv1  33727  esplyfval3  33730  esplyind  33731  fedgmullem1  33786  fedgmullem2  33787  locfinref  33998  esumsnf  34221  hashreprin  34777  poimirlem29  37850  dochpolN  41750  aks6d1c7lem1  42434  evlsbagval  42812  evlsmhpvvval  42838  mhphf  42840  ismrc  42943  mapfzcons  42958  pwssplit4  43331  ntrf2  44365  binomcxplemnn0  44590  fcomptss  45447  fcoss  45454  frexr  45629  climreeq  45859  limccog  45866  limcrecl  45875  limsupre  45885  liminflimsupclim  46051  cncficcgt0  46132  dvdivcncf  46171  dvbdfbdioolem1  46172  ioodvbdlimc1lem1  46175  ioodvbdlimc1lem2  46176  ioodvbdlimc1  46177  ioodvbdlimc2lem  46178  ioodvbdlimc2  46179  dvnprodlem2  46191  voliooicof  46240  volicofmpt  46241  stoweidlem39  46283  stoweidlem59  46303  dirkercncflem3  46349  dirkercncf  46351  fourierdlem48  46398  fourierdlem49  46399  fourierdlem50  46400  fourierdlem51  46401  fourierdlem52  46402  fourierdlem54  46404  fourierdlem59  46409  fourierdlem70  46420  fourierdlem72  46422  fourierdlem73  46423  fourierdlem74  46424  fourierdlem75  46425  fourierdlem76  46426  fourierdlem79  46429  fourierdlem84  46434  fourierdlem85  46435  fourierdlem88  46438  fourierdlem93  46443  fourierdlem94  46444  fourierdlem96  46446  fourierdlem97  46447  fourierdlem98  46448  fourierdlem99  46449  fourierdlem102  46452  fourierdlem103  46453  fourierdlem104  46454  fourierdlem111  46461  fourierdlem112  46462  fourierdlem113  46463  fourierdlem114  46464  fouriercn  46476  elaa2lem  46477  rrxtopnfi  46531  rrndistlt  46534  ioorrnopnlem  46548  issalnnd  46589  fge0icoicc  46609  fge0iccre  46618  sge0isum  46671  sge0gtfsumgt  46687  sge0seq  46690  ismeannd  46711  meaiuninclem  46724  caragenunicl  46768  caratheodorylem1  46770  caratheodorylem2  46771  isomenndlem  46774  elhoi  46786  hoicvr  46792  sge0hsphoire  46833  hoidmv1le  46838  hoiqssbllem3  46868  hspmbllem2  46871  ovolval2lem  46887  ovolval3  46891  ovolval4lem2  46894  ovolval5lem2  46897  ovnovollem1  46900  ovnovollem2  46901  iunhoiioolem  46919  iccvonmbllem  46922  vonioolem2  46925  vonioo  46926  smfco  47046  nnsum3primesgbe  48038  nnsum4primesodd  48042  nnsum4primesoddALTV  48043  grimuhgr  48133  uhgrimisgrgric  48177  isubgr3stgrlem6  48217  1hegrlfgr  48378  funcringcsetcALTV2lem8  48543  funcringcsetclem8ALTV  48566  mapsnop  48590  fprmappr  48591  zlmodzxzel  48601  snlindsntorlem  48716  refdivmptf  48788  refdivmptfv  48792  elbigolo1  48803  2arymaptfo  48900  prelrrx2  48959  line2  48998  line2x  49000  line2y  49001  amgmwlem  50047