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 585	1 ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)

Syntax hints:   → wi 4   ⊆ wss 3890  ⟶wf 6496

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 3907  df-f 6504

This theorem is referenced by:  fconst6g  6731  f1ounsn  7229  fsnex  7240  tposf2  8202  mapsnd  8836  mapss  8839  ralxpmap  8846  ac6sfi  9196  infpwfien  9986  infmap2  10141  cofsmo  10193  fin23lem32  10268  axdc3lem4  10377  pwfseqlem4a  10586  fseq1p1m1  13554  seqf1olem2  14006  wrdlen2i  14906  supcvg  15823  vdwlem8  16961  isacs2  17621  funcres2b  17866  funcestrcsetclem8  18115  funcsetcestrclem8  18130  gsumress  18652  gsumwsubmcl  18807  gsumws1  18808  pj1ghm  19680  gsumval3eu  19881  gsumval3  19884  gsumsubmcl  19896  gsumzadd  19899  gsumzoppg  19921  dprdsn  20015  pwssplit1  21056  pjdm2  21693  evlsvvval  22073  psdmul  22134  mat1dimelbas  22438  cnrest2  23253  cnprest2  23257  1stcelcls  23428  xkoptsub  23621  tsmssubm  24110  cncfss  24868  ipcn  25215  equivcau  25269  lmcau  25282  rrx0el  25367  i1fmulclem  25671  i1fres  25674  mbfi1fseqlem4  25687  itg2mulclem  25715  limccnp  25860  dvcmulf  25914  dvcobr  25915  dvcnvlem  25945  dvcnv  25946  dvef  25949  elply2  26163  plyeq0lem  26177  plyaddlem  26182  plymullem  26183  dgrlem  26196  coeidlem  26204  jensenlem2  26953  jensen  26954  om2noseqlt  28293  om2noseqlt2  28294  om2noseqf1o  28295  umgrupgr  29174  upgr1e  29184  umgrislfupgr  29194  usgrislfuspgr  29258  upgrres1  29384  umgrres1  29385  umgr2v2e  29596  0clwlkv  30203  minvecolem3  30949  minvecolem4  30953  occllem  31376  chscllem2  31711  chscllem4  31713  pjhf  31781  elrgspnsubrunlem1  33310  gsumind  33407  islinds5  33429  ellspds  33430  linds2eq  33443  1arithidomlem2  33598  1arithidom  33599  dfufd2lem  33611  mplmulmvr  33685  psrmonprod  33698  mplgsum  33699  esplyfval0  33710  esplylem  33712  esplympl  33713  esplyfv1  33715  esplyfval3  33718  esplyfval1  33719  esplyfvaln  33720  esplyind  33721  fedgmullem1  33775  fedgmullem2  33776  locfinref  33987  esumsnf  34210  hashreprin  34766  poimirlem29  37972  dochpolN  41938  aks6d1c7lem1  42621  evlsbagval  43004  evlsmhpvvval  43030  mhphf  43032  ismrc  43135  mapfzcons  43150  pwssplit4  43519  ntrf2  44553  binomcxplemnn0  44778  fcomptss  45634  fcoss  45641  frexr  45816  climreeq  46045  limccog  46052  limcrecl  46061  limsupre  46071  liminflimsupclim  46237  cncficcgt0  46318  dvdivcncf  46357  dvbdfbdioolem1  46358  ioodvbdlimc1lem1  46361  ioodvbdlimc1lem2  46362  ioodvbdlimc1  46363  ioodvbdlimc2lem  46364  ioodvbdlimc2  46365  dvnprodlem2  46377  voliooicof  46426  volicofmpt  46427  stoweidlem39  46469  stoweidlem59  46489  dirkercncflem3  46535  dirkercncf  46537  fourierdlem48  46584  fourierdlem49  46585  fourierdlem50  46586  fourierdlem51  46587  fourierdlem52  46588  fourierdlem54  46590  fourierdlem59  46595  fourierdlem70  46606  fourierdlem72  46608  fourierdlem73  46609  fourierdlem74  46610  fourierdlem75  46611  fourierdlem76  46612  fourierdlem79  46615  fourierdlem84  46620  fourierdlem85  46621  fourierdlem88  46624  fourierdlem93  46629  fourierdlem94  46630  fourierdlem96  46632  fourierdlem97  46633  fourierdlem98  46634  fourierdlem99  46635  fourierdlem102  46638  fourierdlem103  46639  fourierdlem104  46640  fourierdlem111  46647  fourierdlem112  46648  fourierdlem113  46649  fourierdlem114  46650  fouriercn  46662  elaa2lem  46663  rrxtopnfi  46717  rrndistlt  46720  ioorrnopnlem  46734  issalnnd  46775  fge0icoicc  46795  fge0iccre  46804  sge0isum  46857  sge0gtfsumgt  46873  sge0seq  46876  ismeannd  46897  meaiuninclem  46910  caragenunicl  46954  caratheodorylem1  46956  caratheodorylem2  46957  isomenndlem  46960  elhoi  46972  sge0hsphoire  47019  hoidmv1le  47024  hoiqssbllem3  47054  hspmbllem2  47057  ovolval2lem  47073  ovolval3  47077  ovolval4lem2  47080  ovolval5lem2  47083  ovnovollem1  47086  ovnovollem2  47087  iunhoiioolem  47105  iccvonmbllem  47108  vonioolem2  47111  vonioo  47112  smfco  47232  nnsum3primesgbe  48270  nnsum4primesodd  48274  nnsum4primesoddALTV  48275  grimuhgr  48365  uhgrimisgrgric  48409  isubgr3stgrlem6  48449  1hegrlfgr  48610  funcringcsetcALTV2lem8  48775  funcringcsetclem8ALTV  48798  mapsnop  48822  fprmappr  48823  zlmodzxzel  48833  snlindsntorlem  48948  refdivmptf  49020  refdivmptfv  49024  elbigolo1  49035  2arymaptfo  49132  prelrrx2  49191  line2  49230  line2x  49232  line2y  49233  amgmwlem  50279