Theorem fssd 6736

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

Syntax hints:   → wi 4   ⊆ wss 3949  ⟶wf 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-f 6548

This theorem is referenced by:  fco3OLD  6752  fconst6g  6781  fsnex  7281  tposf2  8235  mapsnd  8880  mapss  8883  ralxpmap  8890  ac6sfi  9287  infpwfien  10057  infmap2  10213  cofsmo  10264  fin23lem32  10339  axdc3lem4  10448  pwfseqlem4a  10656  fseq1p1m1  13575  seqf1olem2  14008  wrdlen2i  14893  supcvg  15802  vdwlem8  16921  isacs2  17597  funcres2b  17847  funcestrcsetclem8  18099  funcsetcestrclem8  18114  gsumress  18601  gsumwsubmcl  18718  gsumws1  18719  pj1ghm  19571  gsumval3eu  19772  gsumval3  19775  gsumsubmcl  19787  gsumzadd  19790  gsumzoppg  19812  dprdsn  19906  pwssplit1  20670  pjdm2  21266  mat1dimelbas  21973  cnrest2  22790  cnprest2  22794  1stcelcls  22965  xkoptsub  23158  tsmssubm  23647  cncfss  24415  ipcn  24763  equivcau  24817  lmcau  24830  rrx0el  24915  i1fmulclem  25220  i1fres  25223  mbfi1fseqlem4  25236  itg2mulclem  25264  limccnp  25408  dvcmulf  25462  dvcobr  25463  dvcnvlem  25493  dvcnv  25494  dvef  25497  elply2  25710  plyeq0lem  25724  plyaddlem  25729  plymullem  25730  dgrlem  25743  coeidlem  25751  jensenlem2  26492  jensen  26493  umgrupgr  28363  upgr1e  28373  umgrislfupgr  28383  usgrislfuspgr  28444  upgrres1  28570  umgrres1  28571  umgr2v2e  28782  0clwlkv  29384  minvecolem3  30129  minvecolem4  30133  occllem  30556  chscllem2  30891  chscllem4  30893  pjhf  30961  islinds5  32480  ellspds  32481  linds2eq  32497  fedgmullem1  32714  fedgmullem2  32715  locfinref  32821  esumsnf  33062  hashreprin  33632  gg-dvcobr  35176  poimirlem29  36517  dochpolN  40361  evlsvvval  41135  evlsbagval  41138  evlsmhpvvval  41167  mhphf  41169  ismrc  41439  mapfzcons  41454  pwssplit4  41831  ntrf2  42875  binomcxplemnn0  43108  fcomptss  43902  fcoss  43909  frexr  44095  climreeq  44329  limccog  44336  limcrecl  44345  limsupre  44357  liminflimsupclim  44523  cncficcgt0  44604  dvdivcncf  44643  dvbdfbdioolem1  44644  ioodvbdlimc1lem1  44647  ioodvbdlimc1lem2  44648  ioodvbdlimc1  44649  ioodvbdlimc2lem  44650  ioodvbdlimc2  44651  dvnprodlem2  44663  voliooicof  44712  volicofmpt  44713  stoweidlem39  44755  stoweidlem59  44775  dirkercncflem3  44821  dirkercncf  44823  fourierdlem48  44870  fourierdlem49  44871  fourierdlem50  44872  fourierdlem51  44873  fourierdlem52  44874  fourierdlem54  44876  fourierdlem59  44881  fourierdlem70  44892  fourierdlem72  44894  fourierdlem73  44895  fourierdlem74  44896  fourierdlem75  44897  fourierdlem76  44898  fourierdlem79  44901  fourierdlem84  44906  fourierdlem85  44907  fourierdlem88  44910  fourierdlem93  44915  fourierdlem94  44916  fourierdlem96  44918  fourierdlem97  44919  fourierdlem98  44920  fourierdlem99  44921  fourierdlem102  44924  fourierdlem103  44925  fourierdlem104  44926  fourierdlem111  44933  fourierdlem112  44934  fourierdlem113  44935  fourierdlem114  44936  fouriercn  44948  elaa2lem  44949  rrxtopnfi  45003  rrndistlt  45006  ioorrnopnlem  45020  issalnnd  45061  fge0icoicc  45081  fge0iccre  45090  sge0isum  45143  sge0gtfsumgt  45159  sge0seq  45162  ismeannd  45183  meaiuninclem  45196  caragenunicl  45240  caratheodorylem1  45242  caratheodorylem2  45243  isomenndlem  45246  elhoi  45258  hoicvr  45264  sge0hsphoire  45305  hoidmv1le  45310  hoiqssbllem3  45340  hspmbllem2  45343  ovolval2lem  45359  ovolval3  45363  ovolval4lem2  45366  ovolval5lem2  45369  ovnovollem1  45372  ovnovollem2  45373  iunhoiioolem  45391  iccvonmbllem  45394  vonioolem2  45397  vonioo  45398  smfco  45518  nnsum3primesgbe  46460  nnsum4primesodd  46464  nnsum4primesoddALTV  46465  1hegrlfgr  46510  funcringcsetcALTV2lem8  46941  funcringcsetclem8ALTV  46964  mapsnop  47020  fprmappr  47021  zlmodzxzel  47031  snlindsntorlem  47151  refdivmptf  47228  refdivmptfv  47232  elbigolo1  47243  2arymaptfo  47340  prelrrx2  47399  line2  47438  line2x  47440  line2y  47441  amgmwlem  47849