Theorem fssd 6627

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

Syntax hints:   → wi 4   ⊆ wss 3888  ⟶wf 6433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905  df-f 6441

This theorem is referenced by:  fco3OLD  6643  fconst6g  6672  fsnex  7164  tposf2  8075  mapsnd  8683  mapss  8686  ralxpmap  8693  ac6sfi  9067  infpwfien  9827  infmap2  9983  cofsmo  10034  fin23lem32  10109  axdc3lem4  10218  pwfseqlem4a  10426  fseq1p1m1  13339  seqf1olem2  13772  wrdlen2i  14664  supcvg  15577  vdwlem8  16698  isacs2  17371  funcres2b  17621  funcestrcsetclem8  17873  funcsetcestrclem8  17888  gsumress  18375  gsumwsubmcl  18484  gsumws1  18485  pj1ghm  19318  gsumval3eu  19514  gsumval3  19517  gsumsubmcl  19529  gsumzadd  19532  gsumzoppg  19554  dprdsn  19648  pwssplit1  20330  pjdm2  20927  mat1dimelbas  21629  cnrest2  22446  cnprest2  22450  1stcelcls  22621  xkoptsub  22814  tsmssubm  23303  cncfss  24071  ipcn  24419  equivcau  24473  lmcau  24486  rrx0el  24571  i1fmulclem  24876  i1fres  24879  mbfi1fseqlem4  24892  itg2mulclem  24920  limccnp  25064  dvcmulf  25118  dvcobr  25119  dvcnvlem  25149  dvcnv  25150  dvef  25153  elply2  25366  plyeq0lem  25380  plyaddlem  25385  plymullem  25386  dgrlem  25399  coeidlem  25407  jensenlem2  26146  jensen  26147  umgrupgr  27482  upgr1e  27492  umgrislfupgr  27502  usgrislfuspgr  27563  upgrres1  27689  umgrres1  27690  umgr2v2e  27901  0clwlkv  28504  minvecolem3  29247  minvecolem4  29251  occllem  29674  chscllem2  30009  chscllem4  30011  pjhf  30079  islinds5  31572  ellspds  31573  linds2eq  31584  fedgmullem1  31719  fedgmullem2  31720  locfinref  31800  esumsnf  32041  hashreprin  32609  poimirlem29  35815  dochpolN  39511  ismrc  40530  mapfzcons  40545  pwssplit4  40921  ntrf2  41741  binomcxplemnn0  41974  fcomptss  42750  fcoss  42757  frexr  42931  climreeq  43161  limccog  43168  limcrecl  43177  limsupre  43189  liminflimsupclim  43355  cncficcgt0  43436  dvdivcncf  43475  dvbdfbdioolem1  43476  ioodvbdlimc1lem1  43479  ioodvbdlimc1lem2  43480  ioodvbdlimc1  43481  ioodvbdlimc2lem  43482  ioodvbdlimc2  43483  dvnprodlem2  43495  voliooicof  43544  volicofmpt  43545  stoweidlem39  43587  stoweidlem59  43607  dirkercncflem3  43653  dirkercncf  43655  fourierdlem48  43702  fourierdlem49  43703  fourierdlem50  43704  fourierdlem51  43705  fourierdlem52  43706  fourierdlem54  43708  fourierdlem59  43713  fourierdlem70  43724  fourierdlem72  43726  fourierdlem73  43727  fourierdlem74  43728  fourierdlem75  43729  fourierdlem76  43730  fourierdlem79  43733  fourierdlem84  43738  fourierdlem85  43739  fourierdlem88  43742  fourierdlem93  43747  fourierdlem94  43748  fourierdlem96  43750  fourierdlem97  43751  fourierdlem98  43752  fourierdlem99  43753  fourierdlem102  43756  fourierdlem103  43757  fourierdlem104  43758  fourierdlem111  43765  fourierdlem112  43766  fourierdlem113  43767  fourierdlem114  43768  fouriercn  43780  elaa2lem  43781  rrxtopnfi  43835  rrndistlt  43838  ioorrnopnlem  43852  issalnnd  43891  fge0icoicc  43910  fge0iccre  43919  sge0isum  43972  sge0gtfsumgt  43988  sge0seq  43991  ismeannd  44012  meaiuninclem  44025  caragenunicl  44069  caratheodorylem1  44071  caratheodorylem2  44072  isomenndlem  44075  elhoi  44087  hoicvr  44093  sge0hsphoire  44134  hoidmv1le  44139  hoiqssbllem3  44169  hspmbllem2  44172  ovolval2lem  44188  ovolval3  44192  ovolval4lem2  44195  ovolval5lem2  44198  ovolval5lem3  44199  ovnovollem1  44201  ovnovollem2  44202  iunhoiioolem  44220  iccvonmbllem  44223  vonioolem2  44226  vonioo  44227  smfco  44347  nnsum3primesgbe  45255  nnsum4primesodd  45259  nnsum4primesoddALTV  45260  1hegrlfgr  45305  funcringcsetcALTV2lem8  45612  funcringcsetclem8ALTV  45635  mapsnop  45691  fprmappr  45692  zlmodzxzel  45702  snlindsntorlem  45822  refdivmptf  45899  refdivmptfv  45903  elbigolo1  45914  2arymaptfo  46011  prelrrx2  46070  line2  46109  line2x  46111  line2y  46112  amgmwlem  46517