Theorem fssd 6722

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

Syntax hints:   → wi 4   ⊆ wss 3926  ⟶wf 6526

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3943  df-f 6534

This theorem is referenced by:  fconst6g  6766  f1ounsn  7264  fsnex  7275  tposf2  8247  mapsnd  8898  mapss  8901  ralxpmap  8908  ac6sfi  9290  infpwfien  10074  infmap2  10229  cofsmo  10281  fin23lem32  10356  axdc3lem4  10465  pwfseqlem4a  10673  fseq1p1m1  13613  seqf1olem2  14058  wrdlen2i  14959  supcvg  15870  vdwlem8  17006  isacs2  17663  funcres2b  17908  funcestrcsetclem8  18157  funcsetcestrclem8  18172  gsumress  18658  gsumwsubmcl  18813  gsumws1  18814  pj1ghm  19682  gsumval3eu  19883  gsumval3  19886  gsumsubmcl  19898  gsumzadd  19901  gsumzoppg  19923  dprdsn  20017  pwssplit1  21015  pjdm2  21669  psdmul  22102  mat1dimelbas  22407  cnrest2  23222  cnprest2  23226  1stcelcls  23397  xkoptsub  23590  tsmssubm  24079  cncfss  24841  ipcn  25196  equivcau  25250  lmcau  25263  rrx0el  25348  i1fmulclem  25653  i1fres  25656  mbfi1fseqlem4  25669  itg2mulclem  25697  limccnp  25842  dvcmulf  25898  dvcobr  25899  dvcobrOLD  25900  dvcnvlem  25930  dvcnv  25931  dvef  25934  elply2  26151  plyeq0lem  26165  plyaddlem  26170  plymullem  26171  dgrlem  26184  coeidlem  26192  jensenlem2  26948  jensen  26949  om2noseqlt  28222  om2noseqlt2  28223  om2noseqf1o  28224  umgrupgr  29028  upgr1e  29038  umgrislfupgr  29048  usgrislfuspgr  29112  upgrres1  29238  umgrres1  29239  umgr2v2e  29451  0clwlkv  30058  minvecolem3  30803  minvecolem4  30807  occllem  31230  chscllem2  31565  chscllem4  31567  pjhf  31635  elrgspnsubrunlem1  33188  islinds5  33328  ellspds  33329  linds2eq  33342  1arithidomlem2  33497  1arithidom  33498  dfufd2lem  33510  fedgmullem1  33615  fedgmullem2  33616  locfinref  33818  esumsnf  34041  hashreprin  34598  poimirlem29  37619  dochpolN  41455  aks6d1c7lem1  42139  evlsvvval  42533  evlsbagval  42536  evlsmhpvvval  42565  mhphf  42567  ismrc  42671  mapfzcons  42686  pwssplit4  43060  ntrf2  44095  binomcxplemnn0  44321  fcomptss  45175  fcoss  45182  frexr  45360  climreeq  45590  limccog  45597  limcrecl  45606  limsupre  45618  liminflimsupclim  45784  cncficcgt0  45865  dvdivcncf  45904  dvbdfbdioolem1  45905  ioodvbdlimc1lem1  45908  ioodvbdlimc1lem2  45909  ioodvbdlimc1  45910  ioodvbdlimc2lem  45911  ioodvbdlimc2  45912  dvnprodlem2  45924  voliooicof  45973  volicofmpt  45974  stoweidlem39  46016  stoweidlem59  46036  dirkercncflem3  46082  dirkercncf  46084  fourierdlem48  46131  fourierdlem49  46132  fourierdlem50  46133  fourierdlem51  46134  fourierdlem52  46135  fourierdlem54  46137  fourierdlem59  46142  fourierdlem70  46153  fourierdlem72  46155  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem76  46159  fourierdlem79  46162  fourierdlem84  46167  fourierdlem85  46168  fourierdlem88  46171  fourierdlem93  46176  fourierdlem94  46177  fourierdlem96  46179  fourierdlem97  46180  fourierdlem98  46181  fourierdlem99  46182  fourierdlem102  46185  fourierdlem103  46186  fourierdlem104  46187  fourierdlem111  46194  fourierdlem112  46195  fourierdlem113  46196  fourierdlem114  46197  fouriercn  46209  elaa2lem  46210  rrxtopnfi  46264  rrndistlt  46267  ioorrnopnlem  46281  issalnnd  46322  fge0icoicc  46342  fge0iccre  46351  sge0isum  46404  sge0gtfsumgt  46420  sge0seq  46423  ismeannd  46444  meaiuninclem  46457  caragenunicl  46501  caratheodorylem1  46503  caratheodorylem2  46504  isomenndlem  46507  elhoi  46519  hoicvr  46525  sge0hsphoire  46566  hoidmv1le  46571  hoiqssbllem3  46601  hspmbllem2  46604  ovolval2lem  46620  ovolval3  46624  ovolval4lem2  46627  ovolval5lem2  46630  ovnovollem1  46633  ovnovollem2  46634  iunhoiioolem  46652  iccvonmbllem  46655  vonioolem2  46658  vonioo  46659  smfco  46779  nnsum3primesgbe  47754  nnsum4primesodd  47758  nnsum4primesoddALTV  47759  grimuhgr  47848  uhgrimisgrgric  47892  isubgr3stgrlem6  47931  1hegrlfgr  48055  funcringcsetcALTV2lem8  48220  funcringcsetclem8ALTV  48243  mapsnop  48267  fprmappr  48268  zlmodzxzel  48278  snlindsntorlem  48394  refdivmptf  48470  refdivmptfv  48474  elbigolo1  48485  2arymaptfo  48582  prelrrx2  48641  line2  48680  line2x  48682  line2y  48683  amgmwlem  49614