Theorem fssd 6352

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

Syntax hints:   → wi 4   ⊆ wss 3823  ⟶wf 6178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2744

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2753  df-cleq 2765  df-clel 2840  df-in 3830  df-ss 3837  df-f 6186

This theorem is referenced by:  fconst6g  6391  fsnex  6858  tposf2  7713  mapsnd  8242  mapss  8245  ralxpmap  8252  ac6sfi  8551  infpwfien  9276  infmap2  9432  cofsmo  9483  fin23lem32  9558  axdc3lem4  9667  pwfseqlem4a  9875  fseq1p1m1  12791  seqf1olem2  13219  wrdlen2i  14160  supcvg  15065  vdwlem8  16174  isacs2  16776  funcres2b  17019  funcestrcsetclem8  17249  funcsetcestrclem8  17264  gsumress  17738  gsumwsubmcl  17837  gsumws1  17838  pj1ghm  18581  gsumval3eu  18772  gsumval3  18775  gsumsubmcl  18786  gsumzadd  18789  gsumzoppg  18811  dprdsn  18902  pwssplit1  19547  pjdm2  20551  mat1dimelbas  20778  cnrest2  21592  cnprest2  21596  1stcelcls  21767  xkoptsub  21960  tsmssubm  22448  cncfss  23204  ipcn  23546  equivcau  23600  lmcau  23613  rrx0el  23698  i1fmulclem  24000  i1fres  24003  mbfi1fseqlem4  24016  itg2mulclem  24044  limccnp  24186  dvcmulf  24239  dvcobr  24240  dvcnvlem  24270  dvcnv  24271  dvef  24274  elply2  24483  plyeq0lem  24497  plyaddlem  24502  plymullem  24503  dgrlem  24516  coeidlem  24524  jensenlem2  25261  jensen  25262  umgrupgr  26585  upgr1e  26595  umgrislfupgr  26605  usgrislfuspgr  26666  upgrres1  26792  umgrres1  26793  umgr2v2e  27004  0clwlkv  27654  minvecolem3  28425  minvecolem4  28429  occllem  28855  chscllem2  29190  chscllem4  29192  pjhf  29260  islinds5  30605  ellspds  30606  linds2eq  30612  fedgmullem1  30654  fedgmullem2  30655  locfinref  30749  esumsnf  30967  hashreprin  31539  poimirlem29  34362  dochpolN  38071  ismrc  38693  mapfzcons  38708  pwssplit4  39085  ntrf2  39837  binomcxplemnn0  40097  fcomptss  40891  fcoss  40898  fco3  40916  frexr  41085  climreeq  41325  limccog  41332  limcrecl  41341  limsupre  41353  liminflimsupclim  41519  cncficcgt0  41601  dvdivcncf  41642  dvbdfbdioolem1  41643  ioodvbdlimc1lem1  41646  ioodvbdlimc1lem2  41647  ioodvbdlimc1  41648  ioodvbdlimc2lem  41649  ioodvbdlimc2  41650  dvnprodlem2  41662  voliooicof  41712  volicofmpt  41713  stoweidlem39  41755  stoweidlem59  41775  dirkercncflem3  41821  dirkercncf  41823  fourierdlem48  41870  fourierdlem49  41871  fourierdlem50  41872  fourierdlem51  41873  fourierdlem52  41874  fourierdlem54  41876  fourierdlem59  41881  fourierdlem70  41892  fourierdlem72  41894  fourierdlem73  41895  fourierdlem74  41896  fourierdlem75  41897  fourierdlem76  41898  fourierdlem79  41901  fourierdlem84  41906  fourierdlem85  41907  fourierdlem88  41910  fourierdlem93  41915  fourierdlem94  41916  fourierdlem96  41918  fourierdlem97  41919  fourierdlem98  41920  fourierdlem99  41921  fourierdlem102  41924  fourierdlem103  41925  fourierdlem104  41926  fourierdlem111  41933  fourierdlem112  41934  fourierdlem113  41935  fourierdlem114  41936  fouriercn  41948  elaa2lem  41949  rrxtopnfi  42003  rrndistlt  42006  ioorrnopnlem  42020  issalnnd  42059  fge0icoicc  42078  fge0iccre  42087  sge0isum  42140  sge0gtfsumgt  42156  sge0seq  42159  ismeannd  42180  meaiuninclem  42193  caragenunicl  42237  caratheodorylem1  42239  caratheodorylem2  42240  isomenndlem  42243  elhoi  42255  hoicvr  42261  sge0hsphoire  42302  hoidmv1le  42307  hoiqssbllem3  42337  hspmbllem2  42340  ovolval2lem  42356  ovolval3  42360  ovolval4lem2  42363  ovolval5lem2  42366  ovolval5lem3  42367  ovnovollem1  42369  ovnovollem2  42370  iunhoiioolem  42388  iccvonmbllem  42391  vonioolem2  42394  vonioo  42395  smfco  42508  nnsum3primesgbe  43325  nnsum4primesodd  43329  nnsum4primesoddALTV  43330  1hegrlfgr  43375  funcringcsetcALTV2lem8  43678  funcringcsetclem8ALTV  43701  mapsnop  43757  mapprop  43758  zlmodzxzel  43767  snlindsntorlem  43892  refdivmptf  43970  refdivmptfv  43974  elbigolo1  43985  prelrrx2  44068  line2  44107  line2x  44109  line2y  44110  amgmwlem  44270