Theorem fssd 6724

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

Syntax hints:   → wi 4   ⊆ wss 3913  ⟶wf 6533

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ss 3930  df-f 6541

This theorem is referenced by:  fconst6g  6768  f1ounsn  7271  fsnex  7282  tposf2  8245  mapsnd  8883  mapss  8886  ralxpmap  8893  ac6sfi  9243  infpwfien  10045  infmap2  10199  cofsmo  10252  fin23lem32  10327  axdc3lem4  10436  pwfseqlem4a  10645  fseq1p1m1  13625  seqf1olem2  14077  wrdlen2i  14978  supcvg  15909  vdwlem8  17047  isacs2  17708  funcres2b  17953  funcestrcsetclem8  18202  funcsetcestrclem8  18217  gsumress  18739  gsumwsubmcl  18895  gsumws1  18896  pj1ghm  19772  gsumval3eu  19973  gsumval3  19976  gsumsubmcl  19988  gsumzadd  19991  gsumzoppg  20013  dprdsn  20107  pwssplit1  21157  pjdm2  21829  evlsvvval  22212  psdmul  22297  mat1dimelbas  22596  cnrest2  23411  cnprest2  23415  1stcelcls  23586  xkoptsub  23779  tsmssubm  24268  cncfss  25026  ipcn  25373  equivcau  25427  lmcau  25440  rrx0el  25525  i1fmulclem  25829  i1fres  25832  mbfi1fseqlem4  25845  itg2mulclem  25873  limccnp  26018  dvcmulf  26072  dvcobr  26073  dvcnvlem  26103  dvcnv  26104  dvef  26107  elply2  26321  plyeq0lem  26335  plyaddlem  26340  plymullem  26341  dgrlem  26354  coeidlem  26362  jensenlem2  27117  jensen  27118  om2noseqlt  28457  om2noseqlt2  28458  om2noseqf1o  28459  umgrupgr  29393  upgr1e  29403  umgrislfupgr  29413  usgrislfuspgr  29477  upgrres1  29603  umgrres1  29604  umgr2v2e  29815  0clwlkv  30422  minvecolem3  31168  minvecolem4  31172  occllem  31595  chscllem2  31930  chscllem4  31932  pjhf  32000  elrgspnsubrunlem1  33507  gsumind  33607  islinds5  33624  ellspds  33625  linds2eq  33637  1arithidomlem2  33770  1arithidom  33771  dfufd2lem  33783  selvply1rhmlemb  33853  mplmulmvr  33873  psrmonprod  33886  mplgsum  33887  esplyfval0  33898  esplylem  33900  esplympl  33901  esplyfv1  33903  esplyfval3  33906  esplyfval1  33907  esplyfvaln  33908  esplyind  33909  fedgmullem1  33963  fedgmullem2  33964  locfinref  34175  esumsnf  34398  hashreprin  34951  poimirlem29  38187  dochpolN  42153  aks6d1c7lem1  42836  evlsbagval  43209  evlsmhpvvval  43218  mhphf  43220  ismrc  43323  mapfzcons  43338  pwssplit4  43707  ntrf2  44741  binomcxplemnn0  44950  fcomptss  45811  fcoss  45817  frexr  45991  climreeq  46220  limccog  46227  limcrecl  46236  limsupre  46246  liminflimsupclim  46412  cncficcgt0  46493  dvdivcncf  46532  dvbdfbdioolem1  46533  ioodvbdlimc1lem1  46536  ioodvbdlimc1lem2  46537  ioodvbdlimc1  46538  ioodvbdlimc2lem  46539  ioodvbdlimc2  46540  dvnprodlem2  46552  voliooicof  46601  volicofmpt  46602  stoweidlem39  46644  stoweidlem59  46664  dirkercncflem3  46710  dirkercncf  46712  fourierdlem48  46759  fourierdlem49  46760  fourierdlem50  46761  fourierdlem51  46762  fourierdlem52  46763  fourierdlem54  46765  fourierdlem59  46770  fourierdlem70  46781  fourierdlem72  46783  fourierdlem73  46784  fourierdlem74  46785  fourierdlem75  46786  fourierdlem76  46787  fourierdlem79  46790  fourierdlem84  46795  fourierdlem85  46796  fourierdlem88  46799  fourierdlem93  46804  fourierdlem94  46805  fourierdlem96  46807  fourierdlem97  46808  fourierdlem98  46809  fourierdlem99  46810  fourierdlem102  46813  fourierdlem103  46814  fourierdlem104  46815  fourierdlem111  46822  fourierdlem112  46823  fourierdlem113  46824  fourierdlem114  46825  fouriercn  46837  elaa2lem  46838  rrxtopnfi  46892  rrndistlt  46895  ioorrnopnlem  46909  issalnnd  46950  fge0icoicc  46970  fge0iccre  46979  sge0isum  47032  sge0gtfsumgt  47048  sge0seq  47051  ismeannd  47072  meaiuninclem  47085  caragenunicl  47129  caratheodorylem1  47131  caratheodorylem2  47132  isomenndlem  47135  elhoi  47147  sge0hsphoire  47194  hoidmv1le  47199  hoiqssbllem3  47229  hspmbllem2  47232  ovolval2lem  47248  ovolval3  47252  ovolval4lem2  47255  ovolval5lem2  47258  ovnovollem1  47261  ovnovollem2  47262  iunhoiioolem  47280  iccvonmbllem  47283  vonioolem2  47286  vonioo  47287  smfco  47407  nnsum3primesgbe  48445  nnsum4primesodd  48449  nnsum4primesoddALTV  48450  grimuhgr  48540  uhgrimisgrgric  48584  isubgr3stgrlem6  48624  1hegrlfgr  48785  funcringcsetcALTV2lem8  48950  funcringcsetclem8ALTV  48973  mapsnop  49008  fprmappr  49009  zlmodzxzel  49019  snlindsntorlem  49134  refdivmptf  49206  refdivmptfv  49210  elbigolo1  49221  2arymaptfo  49318  prelrrx2  49377  line2  49416  line2x  49418  line2y  49419  amgmwlem  50475