Theorem fssd 6676

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

Syntax hints:   → wi 4   ⊆ wss 3898  ⟶wf 6485

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 3915  df-f 6493

This theorem is referenced by:  fconst6g  6720  f1ounsn  7215  fsnex  7226  tposf2  8189  mapsnd  8820  mapss  8823  ralxpmap  8830  ac6sfi  9179  infpwfien  9964  infmap2  10119  cofsmo  10171  fin23lem32  10246  axdc3lem4  10355  pwfseqlem4a  10563  fseq1p1m1  13505  seqf1olem2  13956  wrdlen2i  14856  supcvg  15770  vdwlem8  16907  isacs2  17567  funcres2b  17812  funcestrcsetclem8  18061  funcsetcestrclem8  18076  gsumress  18598  gsumwsubmcl  18753  gsumws1  18754  pj1ghm  19623  gsumval3eu  19824  gsumval3  19827  gsumsubmcl  19839  gsumzadd  19842  gsumzoppg  19864  dprdsn  19958  pwssplit1  21002  pjdm2  21657  evlsvvval  22039  psdmul  22100  mat1dimelbas  22406  cnrest2  23221  cnprest2  23225  1stcelcls  23396  xkoptsub  23589  tsmssubm  24078  cncfss  24839  ipcn  25193  equivcau  25247  lmcau  25260  rrx0el  25345  i1fmulclem  25650  i1fres  25653  mbfi1fseqlem4  25666  itg2mulclem  25694  limccnp  25839  dvcmulf  25895  dvcobr  25896  dvcobrOLD  25897  dvcnvlem  25927  dvcnv  25928  dvef  25931  elply2  26148  plyeq0lem  26162  plyaddlem  26167  plymullem  26168  dgrlem  26181  coeidlem  26189  jensenlem2  26945  jensen  26946  om2noseqlt  28249  om2noseqlt2  28250  om2noseqf1o  28251  umgrupgr  29102  upgr1e  29112  umgrislfupgr  29122  usgrislfuspgr  29186  upgrres1  29312  umgrres1  29313  umgr2v2e  29525  0clwlkv  30132  minvecolem3  30877  minvecolem4  30881  occllem  31304  chscllem2  31639  chscllem4  31641  pjhf  31709  elrgspnsubrunlem1  33257  gsumind  33354  islinds5  33376  ellspds  33377  linds2eq  33390  1arithidomlem2  33545  1arithidom  33546  dfufd2lem  33558  mplmulmvr  33632  esplyfval0  33650  esplylem  33652  esplympl  33653  esplyfv1  33655  esplyfval3  33658  esplyind  33659  fedgmullem1  33714  fedgmullem2  33715  locfinref  33926  esumsnf  34149  hashreprin  34705  poimirlem29  37762  dochpolN  41662  aks6d1c7lem1  42346  evlsbagval  42727  evlsmhpvvval  42753  mhphf  42755  ismrc  42858  mapfzcons  42873  pwssplit4  43246  ntrf2  44281  binomcxplemnn0  44506  fcomptss  45363  fcoss  45370  frexr  45545  climreeq  45775  limccog  45782  limcrecl  45791  limsupre  45801  liminflimsupclim  45967  cncficcgt0  46048  dvdivcncf  46087  dvbdfbdioolem1  46088  ioodvbdlimc1lem1  46091  ioodvbdlimc1lem2  46092  ioodvbdlimc1  46093  ioodvbdlimc2lem  46094  ioodvbdlimc2  46095  dvnprodlem2  46107  voliooicof  46156  volicofmpt  46157  stoweidlem39  46199  stoweidlem59  46219  dirkercncflem3  46265  dirkercncf  46267  fourierdlem48  46314  fourierdlem49  46315  fourierdlem50  46316  fourierdlem51  46317  fourierdlem52  46318  fourierdlem54  46320  fourierdlem59  46325  fourierdlem70  46336  fourierdlem72  46338  fourierdlem73  46339  fourierdlem74  46340  fourierdlem75  46341  fourierdlem76  46342  fourierdlem79  46345  fourierdlem84  46350  fourierdlem85  46351  fourierdlem88  46354  fourierdlem93  46359  fourierdlem94  46360  fourierdlem96  46362  fourierdlem97  46363  fourierdlem98  46364  fourierdlem99  46365  fourierdlem102  46368  fourierdlem103  46369  fourierdlem104  46370  fourierdlem111  46377  fourierdlem112  46378  fourierdlem113  46379  fourierdlem114  46380  fouriercn  46392  elaa2lem  46393  rrxtopnfi  46447  rrndistlt  46450  ioorrnopnlem  46464  issalnnd  46505  fge0icoicc  46525  fge0iccre  46534  sge0isum  46587  sge0gtfsumgt  46603  sge0seq  46606  ismeannd  46627  meaiuninclem  46640  caragenunicl  46684  caratheodorylem1  46686  caratheodorylem2  46687  isomenndlem  46690  elhoi  46702  hoicvr  46708  sge0hsphoire  46749  hoidmv1le  46754  hoiqssbllem3  46784  hspmbllem2  46787  ovolval2lem  46803  ovolval3  46807  ovolval4lem2  46810  ovolval5lem2  46813  ovnovollem1  46816  ovnovollem2  46817  iunhoiioolem  46835  iccvonmbllem  46838  vonioolem2  46841  vonioo  46842  smfco  46962  nnsum3primesgbe  47954  nnsum4primesodd  47958  nnsum4primesoddALTV  47959  grimuhgr  48049  uhgrimisgrgric  48093  isubgr3stgrlem6  48133  1hegrlfgr  48294  funcringcsetcALTV2lem8  48459  funcringcsetclem8ALTV  48482  mapsnop  48506  fprmappr  48507  zlmodzxzel  48517  snlindsntorlem  48632  refdivmptf  48704  refdivmptfv  48708  elbigolo1  48719  2arymaptfo  48816  prelrrx2  48875  line2  48914  line2x  48916  line2y  48917  amgmwlem  49963