Theorem fssd 6685

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

Syntax hints:   → wi 4   ⊆ wss 3889  ⟶wf 6494

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3906  df-f 6502

This theorem is referenced by:  fconst6g  6729  f1ounsn  7227  fsnex  7238  tposf2  8200  mapsnd  8834  mapss  8837  ralxpmap  8844  ac6sfi  9194  infpwfien  9984  infmap2  10139  cofsmo  10191  fin23lem32  10266  axdc3lem4  10375  pwfseqlem4a  10584  fseq1p1m1  13552  seqf1olem2  14004  wrdlen2i  14904  supcvg  15821  vdwlem8  16959  isacs2  17619  funcres2b  17864  funcestrcsetclem8  18113  funcsetcestrclem8  18128  gsumress  18650  gsumwsubmcl  18805  gsumws1  18806  pj1ghm  19678  gsumval3eu  19879  gsumval3  19882  gsumsubmcl  19894  gsumzadd  19897  gsumzoppg  19919  dprdsn  20013  pwssplit1  21054  pjdm2  21691  evlsvvval  22071  psdmul  22132  mat1dimelbas  22436  cnrest2  23251  cnprest2  23255  1stcelcls  23426  xkoptsub  23619  tsmssubm  24108  cncfss  24866  ipcn  25213  equivcau  25267  lmcau  25280  rrx0el  25365  i1fmulclem  25669  i1fres  25672  mbfi1fseqlem4  25685  itg2mulclem  25713  limccnp  25858  dvcmulf  25912  dvcobr  25913  dvcnvlem  25943  dvcnv  25944  dvef  25947  elply2  26161  plyeq0lem  26175  plyaddlem  26180  plymullem  26181  dgrlem  26194  coeidlem  26202  jensenlem2  26951  jensen  26952  om2noseqlt  28291  om2noseqlt2  28292  om2noseqf1o  28293  umgrupgr  29172  upgr1e  29182  umgrislfupgr  29192  usgrislfuspgr  29256  upgrres1  29382  umgrres1  29383  umgr2v2e  29594  0clwlkv  30201  minvecolem3  30947  minvecolem4  30951  occllem  31374  chscllem2  31709  chscllem4  31711  pjhf  31779  elrgspnsubrunlem1  33308  gsumind  33405  islinds5  33427  ellspds  33428  linds2eq  33441  1arithidomlem2  33596  1arithidom  33597  dfufd2lem  33609  mplmulmvr  33683  psrmonprod  33696  mplgsum  33697  esplyfval0  33708  esplylem  33710  esplympl  33711  esplyfv1  33713  esplyfval3  33716  esplyfval1  33717  esplyfvaln  33718  esplyind  33719  fedgmullem1  33773  fedgmullem2  33774  locfinref  33985  esumsnf  34208  hashreprin  34764  poimirlem29  37970  dochpolN  41936  aks6d1c7lem1  42619  evlsbagval  43002  evlsmhpvvval  43028  mhphf  43030  ismrc  43133  mapfzcons  43148  pwssplit4  43517  ntrf2  44551  binomcxplemnn0  44776  fcomptss  45632  fcoss  45639  frexr  45814  climreeq  46043  limccog  46050  limcrecl  46059  limsupre  46069  liminflimsupclim  46235  cncficcgt0  46316  dvdivcncf  46355  dvbdfbdioolem1  46356  ioodvbdlimc1lem1  46359  ioodvbdlimc1lem2  46360  ioodvbdlimc1  46361  ioodvbdlimc2lem  46362  ioodvbdlimc2  46363  dvnprodlem2  46375  voliooicof  46424  volicofmpt  46425  stoweidlem39  46467  stoweidlem59  46487  dirkercncflem3  46533  dirkercncf  46535  fourierdlem48  46582  fourierdlem49  46583  fourierdlem50  46584  fourierdlem51  46585  fourierdlem52  46586  fourierdlem54  46588  fourierdlem59  46593  fourierdlem70  46604  fourierdlem72  46606  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem79  46613  fourierdlem84  46618  fourierdlem85  46619  fourierdlem88  46622  fourierdlem93  46627  fourierdlem94  46628  fourierdlem96  46630  fourierdlem97  46631  fourierdlem98  46632  fourierdlem99  46633  fourierdlem102  46636  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  fourierdlem112  46646  fourierdlem113  46647  fourierdlem114  46648  fouriercn  46660  elaa2lem  46661  rrxtopnfi  46715  rrndistlt  46718  ioorrnopnlem  46732  issalnnd  46773  fge0icoicc  46793  fge0iccre  46802  sge0isum  46855  sge0gtfsumgt  46871  sge0seq  46874  ismeannd  46895  meaiuninclem  46908  caragenunicl  46952  caratheodorylem1  46954  caratheodorylem2  46955  isomenndlem  46958  elhoi  46970  sge0hsphoire  47017  hoidmv1le  47022  hoiqssbllem3  47052  hspmbllem2  47055  ovolval2lem  47071  ovolval3  47075  ovolval4lem2  47078  ovolval5lem2  47081  ovnovollem1  47084  ovnovollem2  47085  iunhoiioolem  47103  iccvonmbllem  47106  vonioolem2  47109  vonioo  47110  smfco  47230  nnsum3primesgbe  48268  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  grimuhgr  48363  uhgrimisgrgric  48407  isubgr3stgrlem6  48447  1hegrlfgr  48608  funcringcsetcALTV2lem8  48773  funcringcsetclem8ALTV  48796  mapsnop  48820  fprmappr  48821  zlmodzxzel  48831  snlindsntorlem  48946  refdivmptf  49018  refdivmptfv  49022  elbigolo1  49033  2arymaptfo  49130  prelrrx2  49189  line2  49228  line2x  49230  line2y  49231  amgmwlem  50277