Theorem fssd 6672

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

Syntax hints:   → wi 4   ⊆ wss 3883  ⟶wf 6481

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-ss 3900  df-f 6489

This theorem is referenced by:  fconst6g  6716  f1ounsn  7216  fsnex  7227  tposf2  8190  mapsnd  8824  mapss  8827  ralxpmap  8834  ac6sfi  9184  infpwfien  9975  infmap2  10130  cofsmo  10182  fin23lem32  10257  axdc3lem4  10366  pwfseqlem4a  10575  fseq1p1m1  13543  seqf1olem2  13995  wrdlen2i  14895  supcvg  15812  vdwlem8  16950  isacs2  17610  funcres2b  17855  funcestrcsetclem8  18104  funcsetcestrclem8  18119  gsumress  18641  gsumwsubmcl  18796  gsumws1  18797  pj1ghm  19669  gsumval3eu  19870  gsumval3  19873  gsumsubmcl  19885  gsumzadd  19888  gsumzoppg  19910  dprdsn  20004  pwssplit1  21049  pjdm2  21686  evlsvvval  22069  psdmul  22154  mat1dimelbas  22454  cnrest2  23269  cnprest2  23273  1stcelcls  23444  xkoptsub  23637  tsmssubm  24126  cncfss  24884  ipcn  25231  equivcau  25285  lmcau  25298  rrx0el  25383  i1fmulclem  25687  i1fres  25690  mbfi1fseqlem4  25703  itg2mulclem  25731  limccnp  25876  dvcmulf  25930  dvcobr  25931  dvcnvlem  25961  dvcnv  25962  dvef  25965  elply2  26179  plyeq0lem  26193  plyaddlem  26198  plymullem  26199  dgrlem  26212  coeidlem  26220  jensenlem2  26969  jensen  26970  om2noseqlt  28309  om2noseqlt2  28310  om2noseqf1o  28311  umgrupgr  29190  upgr1e  29200  umgrislfupgr  29210  usgrislfuspgr  29274  upgrres1  29400  umgrres1  29401  umgr2v2e  29612  0clwlkv  30219  minvecolem3  30965  minvecolem4  30969  occllem  31392  chscllem2  31727  chscllem4  31729  pjhf  31797  elrgspnsubrunlem1  33328  gsumind  33428  islinds5  33450  ellspds  33451  linds2eq  33464  1arithidomlem2  33619  1arithidom  33620  dfufd2lem  33632  selvply1rhmlemb  33703  mplmulmvr  33723  psrmonprod  33736  mplgsum  33737  esplyfval0  33748  esplylem  33750  esplympl  33751  esplyfv1  33753  esplyfval3  33756  esplyfval1  33757  esplyfvaln  33758  esplyind  33759  fedgmullem1  33813  fedgmullem2  33814  locfinref  34025  esumsnf  34248  hashreprin  34804  poimirlem29  38016  dochpolN  41982  aks6d1c7lem1  42665  evlsbagval  43036  evlsmhpvvval  43045  mhphf  43047  ismrc  43150  mapfzcons  43165  pwssplit4  43534  ntrf2  44568  binomcxplemnn0  44793  fcomptss  45649  fcoss  45655  frexr  45829  climreeq  46058  limccog  46065  limcrecl  46074  limsupre  46084  liminflimsupclim  46250  cncficcgt0  46331  dvdivcncf  46370  dvbdfbdioolem1  46371  ioodvbdlimc1lem1  46374  ioodvbdlimc1lem2  46375  ioodvbdlimc1  46376  ioodvbdlimc2lem  46377  ioodvbdlimc2  46378  dvnprodlem2  46390  voliooicof  46439  volicofmpt  46440  stoweidlem39  46482  stoweidlem59  46502  dirkercncflem3  46548  dirkercncf  46550  fourierdlem48  46597  fourierdlem49  46598  fourierdlem50  46599  fourierdlem51  46600  fourierdlem52  46601  fourierdlem54  46603  fourierdlem59  46608  fourierdlem70  46619  fourierdlem72  46621  fourierdlem73  46622  fourierdlem74  46623  fourierdlem75  46624  fourierdlem76  46625  fourierdlem79  46628  fourierdlem84  46633  fourierdlem85  46634  fourierdlem88  46637  fourierdlem93  46642  fourierdlem94  46643  fourierdlem96  46645  fourierdlem97  46646  fourierdlem98  46647  fourierdlem99  46648  fourierdlem102  46651  fourierdlem103  46652  fourierdlem104  46653  fourierdlem111  46660  fourierdlem112  46661  fourierdlem113  46662  fourierdlem114  46663  fouriercn  46675  elaa2lem  46676  rrxtopnfi  46730  rrndistlt  46733  ioorrnopnlem  46747  issalnnd  46788  fge0icoicc  46808  fge0iccre  46817  sge0isum  46870  sge0gtfsumgt  46886  sge0seq  46889  ismeannd  46910  meaiuninclem  46923  caragenunicl  46967  caratheodorylem1  46969  caratheodorylem2  46970  isomenndlem  46973  elhoi  46985  sge0hsphoire  47032  hoidmv1le  47037  hoiqssbllem3  47067  hspmbllem2  47070  ovolval2lem  47086  ovolval3  47090  ovolval4lem2  47093  ovolval5lem2  47096  ovnovollem1  47099  ovnovollem2  47100  iunhoiioolem  47118  iccvonmbllem  47121  vonioolem2  47124  vonioo  47125  smfco  47245  nnsum3primesgbe  48283  nnsum4primesodd  48287  nnsum4primesoddALTV  48288  grimuhgr  48378  uhgrimisgrgric  48422  isubgr3stgrlem6  48462  1hegrlfgr  48623  funcringcsetcALTV2lem8  48788  funcringcsetclem8ALTV  48811  mapsnop  48835  fprmappr  48836  zlmodzxzel  48846  snlindsntorlem  48961  refdivmptf  49033  refdivmptfv  49037  elbigolo1  49048  2arymaptfo  49145  prelrrx2  49204  line2  49243  line2x  49245  line2y  49246  amgmwlem  50292