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 584	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 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964  df-f 6544

This theorem is referenced by:  fco3OLD  6748  fconst6g  6777  fsnex  7277  tposf2  8231  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  19565  gsumval3eu  19766  gsumval3  19769  gsumsubmcl  19781  gsumzadd  19784  gsumzoppg  19806  dprdsn  19900  pwssplit1  20662  pjdm2  21257  mat1dimelbas  21964  cnrest2  22781  cnprest2  22785  1stcelcls  22956  xkoptsub  23149  tsmssubm  23638  cncfss  24406  ipcn  24754  equivcau  24808  lmcau  24821  rrx0el  24906  i1fmulclem  25211  i1fres  25214  mbfi1fseqlem4  25227  itg2mulclem  25255  limccnp  25399  dvcmulf  25453  dvcobr  25454  dvcnvlem  25484  dvcnv  25485  dvef  25488  elply2  25701  plyeq0lem  25715  plyaddlem  25720  plymullem  25721  dgrlem  25734  coeidlem  25742  jensenlem2  26481  jensen  26482  umgrupgr  28352  upgr1e  28362  umgrislfupgr  28372  usgrislfuspgr  28433  upgrres1  28559  umgrres1  28560  umgr2v2e  28771  0clwlkv  29373  minvecolem3  30116  minvecolem4  30120  occllem  30543  chscllem2  30878  chscllem4  30880  pjhf  30948  islinds5  32468  ellspds  32469  linds2eq  32485  fedgmullem1  32702  fedgmullem2  32703  locfinref  32809  esumsnf  33050  hashreprin  33620  gg-dvcobr  35164  poimirlem29  36505  dochpolN  40349  evlsvvval  41132  evlsbagval  41135  evlsmhpvvval  41164  mhphf  41166  ismrc  41424  mapfzcons  41439  pwssplit4  41816  ntrf2  42860  binomcxplemnn0  43093  fcomptss  43887  fcoss  43894  frexr  44081  climreeq  44315  limccog  44322  limcrecl  44331  limsupre  44343  liminflimsupclim  44509  cncficcgt0  44590  dvdivcncf  44629  dvbdfbdioolem1  44630  ioodvbdlimc1lem1  44633  ioodvbdlimc1lem2  44634  ioodvbdlimc1  44635  ioodvbdlimc2lem  44636  ioodvbdlimc2  44637  dvnprodlem2  44649  voliooicof  44698  volicofmpt  44699  stoweidlem39  44741  stoweidlem59  44761  dirkercncflem3  44807  dirkercncf  44809  fourierdlem48  44856  fourierdlem49  44857  fourierdlem50  44858  fourierdlem51  44859  fourierdlem52  44860  fourierdlem54  44862  fourierdlem59  44867  fourierdlem70  44878  fourierdlem72  44880  fourierdlem73  44881  fourierdlem74  44882  fourierdlem75  44883  fourierdlem76  44884  fourierdlem79  44887  fourierdlem84  44892  fourierdlem85  44893  fourierdlem88  44896  fourierdlem93  44901  fourierdlem94  44902  fourierdlem96  44904  fourierdlem97  44905  fourierdlem98  44906  fourierdlem99  44907  fourierdlem102  44910  fourierdlem103  44911  fourierdlem104  44912  fourierdlem111  44919  fourierdlem112  44920  fourierdlem113  44921  fourierdlem114  44922  fouriercn  44934  elaa2lem  44935  rrxtopnfi  44989  rrndistlt  44992  ioorrnopnlem  45006  issalnnd  45047  fge0icoicc  45067  fge0iccre  45076  sge0isum  45129  sge0gtfsumgt  45145  sge0seq  45148  ismeannd  45169  meaiuninclem  45182  caragenunicl  45226  caratheodorylem1  45228  caratheodorylem2  45229  isomenndlem  45232  elhoi  45244  hoicvr  45250  sge0hsphoire  45291  hoidmv1le  45296  hoiqssbllem3  45326  hspmbllem2  45329  ovolval2lem  45345  ovolval3  45349  ovolval4lem2  45352  ovolval5lem2  45355  ovnovollem1  45358  ovnovollem2  45359  iunhoiioolem  45377  iccvonmbllem  45380  vonioolem2  45383  vonioo  45384  smfco  45504  nnsum3primesgbe  46446  nnsum4primesodd  46450  nnsum4primesoddALTV  46451  1hegrlfgr  46496  funcringcsetcALTV2lem8  46894  funcringcsetclem8ALTV  46917  mapsnop  46973  fprmappr  46974  zlmodzxzel  46984  snlindsntorlem  47104  refdivmptf  47181  refdivmptfv  47185  elbigolo1  47196  2arymaptfo  47293  prelrrx2  47352  line2  47391  line2x  47393  line2y  47394  amgmwlem  47802