Theorem fssd 6687

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

Syntax hints:   → wi 4   ⊆ wss 3911  ⟶wf 6495

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3928  df-f 6503

This theorem is referenced by:  fconst6g  6731  f1ounsn  7229  fsnex  7240  tposf2  8206  mapsnd  8836  mapss  8839  ralxpmap  8846  ac6sfi  9207  infpwfien  9991  infmap2  10146  cofsmo  10198  fin23lem32  10273  axdc3lem4  10382  pwfseqlem4a  10590  fseq1p1m1  13535  seqf1olem2  13983  wrdlen2i  14884  supcvg  15798  vdwlem8  16935  isacs2  17590  funcres2b  17835  funcestrcsetclem8  18084  funcsetcestrclem8  18099  gsumress  18585  gsumwsubmcl  18740  gsumws1  18741  pj1ghm  19609  gsumval3eu  19810  gsumval3  19813  gsumsubmcl  19825  gsumzadd  19828  gsumzoppg  19850  dprdsn  19944  pwssplit1  20942  pjdm2  21596  psdmul  22029  mat1dimelbas  22334  cnrest2  23149  cnprest2  23153  1stcelcls  23324  xkoptsub  23517  tsmssubm  24006  cncfss  24768  ipcn  25122  equivcau  25176  lmcau  25189  rrx0el  25274  i1fmulclem  25579  i1fres  25582  mbfi1fseqlem4  25595  itg2mulclem  25623  limccnp  25768  dvcmulf  25824  dvcobr  25825  dvcobrOLD  25826  dvcnvlem  25856  dvcnv  25857  dvef  25860  elply2  26077  plyeq0lem  26091  plyaddlem  26096  plymullem  26097  dgrlem  26110  coeidlem  26118  jensenlem2  26874  jensen  26875  om2noseqlt  28169  om2noseqlt2  28170  om2noseqf1o  28171  umgrupgr  29006  upgr1e  29016  umgrislfupgr  29026  usgrislfuspgr  29090  upgrres1  29216  umgrres1  29217  umgr2v2e  29429  0clwlkv  30033  minvecolem3  30778  minvecolem4  30782  occllem  31205  chscllem2  31540  chscllem4  31542  pjhf  31610  elrgspnsubrunlem1  33171  islinds5  33311  ellspds  33312  linds2eq  33325  1arithidomlem2  33480  1arithidom  33481  dfufd2lem  33493  fedgmullem1  33598  fedgmullem2  33599  locfinref  33804  esumsnf  34027  hashreprin  34584  poimirlem29  37616  dochpolN  41457  aks6d1c7lem1  42141  evlsvvval  42524  evlsbagval  42527  evlsmhpvvval  42556  mhphf  42558  ismrc  42662  mapfzcons  42677  pwssplit4  43051  ntrf2  44086  binomcxplemnn0  44311  fcomptss  45170  fcoss  45177  frexr  45354  climreeq  45584  limccog  45591  limcrecl  45600  limsupre  45612  liminflimsupclim  45778  cncficcgt0  45859  dvdivcncf  45898  dvbdfbdioolem1  45899  ioodvbdlimc1lem1  45902  ioodvbdlimc1lem2  45903  ioodvbdlimc1  45904  ioodvbdlimc2lem  45905  ioodvbdlimc2  45906  dvnprodlem2  45918  voliooicof  45967  volicofmpt  45968  stoweidlem39  46010  stoweidlem59  46030  dirkercncflem3  46076  dirkercncf  46078  fourierdlem48  46125  fourierdlem49  46126  fourierdlem50  46127  fourierdlem51  46128  fourierdlem52  46129  fourierdlem54  46131  fourierdlem59  46136  fourierdlem70  46147  fourierdlem72  46149  fourierdlem73  46150  fourierdlem74  46151  fourierdlem75  46152  fourierdlem76  46153  fourierdlem79  46156  fourierdlem84  46161  fourierdlem85  46162  fourierdlem88  46165  fourierdlem93  46170  fourierdlem94  46171  fourierdlem96  46173  fourierdlem97  46174  fourierdlem98  46175  fourierdlem99  46176  fourierdlem102  46179  fourierdlem103  46180  fourierdlem104  46181  fourierdlem111  46188  fourierdlem112  46189  fourierdlem113  46190  fourierdlem114  46191  fouriercn  46203  elaa2lem  46204  rrxtopnfi  46258  rrndistlt  46261  ioorrnopnlem  46275  issalnnd  46316  fge0icoicc  46336  fge0iccre  46345  sge0isum  46398  sge0gtfsumgt  46414  sge0seq  46417  ismeannd  46438  meaiuninclem  46451  caragenunicl  46495  caratheodorylem1  46497  caratheodorylem2  46498  isomenndlem  46501  elhoi  46513  hoicvr  46519  sge0hsphoire  46560  hoidmv1le  46565  hoiqssbllem3  46595  hspmbllem2  46598  ovolval2lem  46614  ovolval3  46618  ovolval4lem2  46621  ovolval5lem2  46624  ovnovollem1  46627  ovnovollem2  46628  iunhoiioolem  46646  iccvonmbllem  46649  vonioolem2  46652  vonioo  46653  smfco  46773  nnsum3primesgbe  47766  nnsum4primesodd  47770  nnsum4primesoddALTV  47771  grimuhgr  47860  uhgrimisgrgric  47904  isubgr3stgrlem6  47943  1hegrlfgr  48093  funcringcsetcALTV2lem8  48258  funcringcsetclem8ALTV  48281  mapsnop  48305  fprmappr  48306  zlmodzxzel  48316  snlindsntorlem  48432  refdivmptf  48504  refdivmptfv  48508  elbigolo1  48519  2arymaptfo  48616  prelrrx2  48675  line2  48714  line2x  48716  line2y  48717  amgmwlem  49764