Theorem fssd 6732

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

Syntax hints:   → wi 4   ⊆ wss 3947  ⟶wf 6536

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 3954  df-ss 3964  df-f 6544

This theorem is referenced by:  fco3OLD  6748  fconst6g  6777  fsnex  7276  tposf2  8230  mapsnd  8876  mapss  8879  ralxpmap  8886  ac6sfi  9283  infpwfien  10053  infmap2  10209  cofsmo  10260  fin23lem32  10335  axdc3lem4  10444  pwfseqlem4a  10652  fseq1p1m1  13571  seqf1olem2  14004  wrdlen2i  14889  supcvg  15798  vdwlem8  16917  isacs2  17593  funcres2b  17843  funcestrcsetclem8  18095  funcsetcestrclem8  18110  gsumress  18597  gsumwsubmcl  18714  gsumws1  18715  pj1ghm  19564  gsumval3eu  19764  gsumval3  19767  gsumsubmcl  19779  gsumzadd  19782  gsumzoppg  19804  dprdsn  19898  pwssplit1  20658  pjdm2  21250  mat1dimelbas  21955  cnrest2  22772  cnprest2  22776  1stcelcls  22947  xkoptsub  23140  tsmssubm  23629  cncfss  24397  ipcn  24745  equivcau  24799  lmcau  24812  rrx0el  24897  i1fmulclem  25202  i1fres  25205  mbfi1fseqlem4  25218  itg2mulclem  25246  limccnp  25390  dvcmulf  25444  dvcobr  25445  dvcnvlem  25475  dvcnv  25476  dvef  25479  elply2  25692  plyeq0lem  25706  plyaddlem  25711  plymullem  25712  dgrlem  25725  coeidlem  25733  jensenlem2  26472  jensen  26473  umgrupgr  28343  upgr1e  28353  umgrislfupgr  28363  usgrislfuspgr  28424  upgrres1  28550  umgrres1  28551  umgr2v2e  28762  0clwlkv  29364  minvecolem3  30107  minvecolem4  30111  occllem  30534  chscllem2  30869  chscllem4  30871  pjhf  30939  islinds5  32449  ellspds  32450  linds2eq  32462  fedgmullem1  32659  fedgmullem2  32660  locfinref  32759  esumsnf  33000  hashreprin  33570  gg-dvcobr  35114  poimirlem29  36455  dochpolN  40299  evlsvvval  41085  evlsbagval  41088  evlsmhpvvval  41117  mhphf  41119  ismrc  41372  mapfzcons  41387  pwssplit4  41764  ntrf2  42808  binomcxplemnn0  43041  fcomptss  43835  fcoss  43842  frexr  44030  climreeq  44264  limccog  44271  limcrecl  44280  limsupre  44292  liminflimsupclim  44458  cncficcgt0  44539  dvdivcncf  44578  dvbdfbdioolem1  44579  ioodvbdlimc1lem1  44582  ioodvbdlimc1lem2  44583  ioodvbdlimc1  44584  ioodvbdlimc2lem  44585  ioodvbdlimc2  44586  dvnprodlem2  44598  voliooicof  44647  volicofmpt  44648  stoweidlem39  44690  stoweidlem59  44710  dirkercncflem3  44756  dirkercncf  44758  fourierdlem48  44805  fourierdlem49  44806  fourierdlem50  44807  fourierdlem51  44808  fourierdlem52  44809  fourierdlem54  44811  fourierdlem59  44816  fourierdlem70  44827  fourierdlem72  44829  fourierdlem73  44830  fourierdlem74  44831  fourierdlem75  44832  fourierdlem76  44833  fourierdlem79  44836  fourierdlem84  44841  fourierdlem85  44842  fourierdlem88  44845  fourierdlem93  44850  fourierdlem94  44851  fourierdlem96  44853  fourierdlem97  44854  fourierdlem98  44855  fourierdlem99  44856  fourierdlem102  44859  fourierdlem103  44860  fourierdlem104  44861  fourierdlem111  44868  fourierdlem112  44869  fourierdlem113  44870  fourierdlem114  44871  fouriercn  44883  elaa2lem  44884  rrxtopnfi  44938  rrndistlt  44941  ioorrnopnlem  44955  issalnnd  44996  fge0icoicc  45016  fge0iccre  45025  sge0isum  45078  sge0gtfsumgt  45094  sge0seq  45097  ismeannd  45118  meaiuninclem  45131  caragenunicl  45175  caratheodorylem1  45177  caratheodorylem2  45178  isomenndlem  45181  elhoi  45193  hoicvr  45199  sge0hsphoire  45240  hoidmv1le  45245  hoiqssbllem3  45275  hspmbllem2  45278  ovolval2lem  45294  ovolval3  45298  ovolval4lem2  45301  ovolval5lem2  45304  ovnovollem1  45307  ovnovollem2  45308  iunhoiioolem  45326  iccvonmbllem  45329  vonioolem2  45332  vonioo  45333  smfco  45453  nnsum3primesgbe  46395  nnsum4primesodd  46399  nnsum4primesoddALTV  46400  1hegrlfgr  46445  funcringcsetcALTV2lem8  46843  funcringcsetclem8ALTV  46866  mapsnop  46922  fprmappr  46923  zlmodzxzel  46933  snlindsntorlem  47053  refdivmptf  47130  refdivmptfv  47134  elbigolo1  47145  2arymaptfo  47242  prelrrx2  47301  line2  47340  line2x  47342  line2y  47343  amgmwlem  47751