Theorem fssd 6753

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

Syntax hints:   → wi 4   ⊆ wss 3951  ⟶wf 6557

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 3968  df-f 6565

This theorem is referenced by:  fconst6g  6797  f1ounsn  7292  fsnex  7303  tposf2  8275  mapsnd  8926  mapss  8929  ralxpmap  8936  ac6sfi  9320  infpwfien  10102  infmap2  10257  cofsmo  10309  fin23lem32  10384  axdc3lem4  10493  pwfseqlem4a  10701  fseq1p1m1  13638  seqf1olem2  14083  wrdlen2i  14981  supcvg  15892  vdwlem8  17026  isacs2  17696  funcres2b  17942  funcestrcsetclem8  18192  funcsetcestrclem8  18207  gsumress  18695  gsumwsubmcl  18850  gsumws1  18851  pj1ghm  19721  gsumval3eu  19922  gsumval3  19925  gsumsubmcl  19937  gsumzadd  19940  gsumzoppg  19962  dprdsn  20056  pwssplit1  21058  pjdm2  21731  psdmul  22170  mat1dimelbas  22477  cnrest2  23294  cnprest2  23298  1stcelcls  23469  xkoptsub  23662  tsmssubm  24151  cncfss  24925  ipcn  25280  equivcau  25334  lmcau  25347  rrx0el  25432  i1fmulclem  25737  i1fres  25740  mbfi1fseqlem4  25753  itg2mulclem  25781  limccnp  25926  dvcmulf  25982  dvcobr  25983  dvcobrOLD  25984  dvcnvlem  26014  dvcnv  26015  dvef  26018  elply2  26235  plyeq0lem  26249  plyaddlem  26254  plymullem  26255  dgrlem  26268  coeidlem  26276  jensenlem2  27031  jensen  27032  om2noseqlt  28305  om2noseqlt2  28306  om2noseqf1o  28307  umgrupgr  29120  upgr1e  29130  umgrislfupgr  29140  usgrislfuspgr  29204  upgrres1  29330  umgrres1  29331  umgr2v2e  29543  0clwlkv  30150  minvecolem3  30895  minvecolem4  30899  occllem  31322  chscllem2  31657  chscllem4  31659  pjhf  31727  elrgspnsubrunlem1  33251  islinds5  33395  ellspds  33396  linds2eq  33409  1arithidomlem2  33564  1arithidom  33565  dfufd2lem  33577  fedgmullem1  33680  fedgmullem2  33681  locfinref  33840  esumsnf  34065  hashreprin  34635  poimirlem29  37656  dochpolN  41492  aks6d1c7lem1  42181  evlsvvval  42573  evlsbagval  42576  evlsmhpvvval  42605  mhphf  42607  ismrc  42712  mapfzcons  42727  pwssplit4  43101  ntrf2  44137  binomcxplemnn0  44368  fcomptss  45208  fcoss  45215  frexr  45396  climreeq  45628  limccog  45635  limcrecl  45644  limsupre  45656  liminflimsupclim  45822  cncficcgt0  45903  dvdivcncf  45942  dvbdfbdioolem1  45943  ioodvbdlimc1lem1  45946  ioodvbdlimc1lem2  45947  ioodvbdlimc1  45948  ioodvbdlimc2lem  45949  ioodvbdlimc2  45950  dvnprodlem2  45962  voliooicof  46011  volicofmpt  46012  stoweidlem39  46054  stoweidlem59  46074  dirkercncflem3  46120  dirkercncf  46122  fourierdlem48  46169  fourierdlem49  46170  fourierdlem50  46171  fourierdlem51  46172  fourierdlem52  46173  fourierdlem54  46175  fourierdlem59  46180  fourierdlem70  46191  fourierdlem72  46193  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem76  46197  fourierdlem79  46200  fourierdlem84  46205  fourierdlem85  46206  fourierdlem88  46209  fourierdlem93  46214  fourierdlem94  46215  fourierdlem96  46217  fourierdlem97  46218  fourierdlem98  46219  fourierdlem99  46220  fourierdlem102  46223  fourierdlem103  46224  fourierdlem104  46225  fourierdlem111  46232  fourierdlem112  46233  fourierdlem113  46234  fourierdlem114  46235  fouriercn  46247  elaa2lem  46248  rrxtopnfi  46302  rrndistlt  46305  ioorrnopnlem  46319  issalnnd  46360  fge0icoicc  46380  fge0iccre  46389  sge0isum  46442  sge0gtfsumgt  46458  sge0seq  46461  ismeannd  46482  meaiuninclem  46495  caragenunicl  46539  caratheodorylem1  46541  caratheodorylem2  46542  isomenndlem  46545  elhoi  46557  hoicvr  46563  sge0hsphoire  46604  hoidmv1le  46609  hoiqssbllem3  46639  hspmbllem2  46642  ovolval2lem  46658  ovolval3  46662  ovolval4lem2  46665  ovolval5lem2  46668  ovnovollem1  46671  ovnovollem2  46672  iunhoiioolem  46690  iccvonmbllem  46693  vonioolem2  46696  vonioo  46697  smfco  46817  nnsum3primesgbe  47779  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  grimuhgr  47878  uhgrimisgrgric  47899  isubgr3stgrlem6  47938  1hegrlfgr  48048  funcringcsetcALTV2lem8  48213  funcringcsetclem8ALTV  48236  mapsnop  48260  fprmappr  48261  zlmodzxzel  48271  snlindsntorlem  48387  refdivmptf  48463  refdivmptfv  48467  elbigolo1  48478  2arymaptfo  48575  prelrrx2  48634  line2  48673  line2x  48675  line2y  48676  amgmwlem  49321