Theorem fssd 6563

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

Syntax hints:   → wi 4   ⊆ wss 3866  ⟶wf 6376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873  df-ss 3883  df-f 6384

This theorem is referenced by:  fco3OLD  6579  fconst6g  6608  fsnex  7093  tposf2  7992  mapsnd  8567  mapss  8570  ralxpmap  8577  ac6sfi  8915  infpwfien  9676  infmap2  9832  cofsmo  9883  fin23lem32  9958  axdc3lem4  10067  pwfseqlem4a  10275  fseq1p1m1  13186  seqf1olem2  13616  wrdlen2i  14507  supcvg  15420  vdwlem8  16541  isacs2  17156  funcres2b  17403  funcestrcsetclem8  17654  funcsetcestrclem8  17669  gsumress  18154  gsumwsubmcl  18263  gsumws1  18264  pj1ghm  19093  gsumval3eu  19289  gsumval3  19292  gsumsubmcl  19304  gsumzadd  19307  gsumzoppg  19329  dprdsn  19423  pwssplit1  20096  pjdm2  20673  mat1dimelbas  21368  cnrest2  22183  cnprest2  22187  1stcelcls  22358  xkoptsub  22551  tsmssubm  23040  cncfss  23796  ipcn  24143  equivcau  24197  lmcau  24210  rrx0el  24295  i1fmulclem  24600  i1fres  24603  mbfi1fseqlem4  24616  itg2mulclem  24644  limccnp  24788  dvcmulf  24842  dvcobr  24843  dvcnvlem  24873  dvcnv  24874  dvef  24877  elply2  25090  plyeq0lem  25104  plyaddlem  25109  plymullem  25110  dgrlem  25123  coeidlem  25131  jensenlem2  25870  jensen  25871  umgrupgr  27194  upgr1e  27204  umgrislfupgr  27214  usgrislfuspgr  27275  upgrres1  27401  umgrres1  27402  umgr2v2e  27613  0clwlkv  28214  minvecolem3  28957  minvecolem4  28961  occllem  29384  chscllem2  29719  chscllem4  29721  pjhf  29789  islinds5  31277  ellspds  31278  linds2eq  31289  fedgmullem1  31424  fedgmullem2  31425  locfinref  31505  esumsnf  31744  hashreprin  32312  poimirlem29  35543  dochpolN  39241  ismrc  40226  mapfzcons  40241  pwssplit4  40617  ntrf2  41411  binomcxplemnn0  41640  fcomptss  42416  fcoss  42423  frexr  42597  climreeq  42829  limccog  42836  limcrecl  42845  limsupre  42857  liminflimsupclim  43023  cncficcgt0  43104  dvdivcncf  43143  dvbdfbdioolem1  43144  ioodvbdlimc1lem1  43147  ioodvbdlimc1lem2  43148  ioodvbdlimc1  43149  ioodvbdlimc2lem  43150  ioodvbdlimc2  43151  dvnprodlem2  43163  voliooicof  43212  volicofmpt  43213  stoweidlem39  43255  stoweidlem59  43275  dirkercncflem3  43321  dirkercncf  43323  fourierdlem48  43370  fourierdlem49  43371  fourierdlem50  43372  fourierdlem51  43373  fourierdlem52  43374  fourierdlem54  43376  fourierdlem59  43381  fourierdlem70  43392  fourierdlem72  43394  fourierdlem73  43395  fourierdlem74  43396  fourierdlem75  43397  fourierdlem76  43398  fourierdlem79  43401  fourierdlem84  43406  fourierdlem85  43407  fourierdlem88  43410  fourierdlem93  43415  fourierdlem94  43416  fourierdlem96  43418  fourierdlem97  43419  fourierdlem98  43420  fourierdlem99  43421  fourierdlem102  43424  fourierdlem103  43425  fourierdlem104  43426  fourierdlem111  43433  fourierdlem112  43434  fourierdlem113  43435  fourierdlem114  43436  fouriercn  43448  elaa2lem  43449  rrxtopnfi  43503  rrndistlt  43506  ioorrnopnlem  43520  issalnnd  43559  fge0icoicc  43578  fge0iccre  43587  sge0isum  43640  sge0gtfsumgt  43656  sge0seq  43659  ismeannd  43680  meaiuninclem  43693  caragenunicl  43737  caratheodorylem1  43739  caratheodorylem2  43740  isomenndlem  43743  elhoi  43755  hoicvr  43761  sge0hsphoire  43802  hoidmv1le  43807  hoiqssbllem3  43837  hspmbllem2  43840  ovolval2lem  43856  ovolval3  43860  ovolval4lem2  43863  ovolval5lem2  43866  ovolval5lem3  43867  ovnovollem1  43869  ovnovollem2  43870  iunhoiioolem  43888  iccvonmbllem  43891  vonioolem2  43894  vonioo  43895  smfco  44008  nnsum3primesgbe  44917  nnsum4primesodd  44921  nnsum4primesoddALTV  44922  1hegrlfgr  44967  funcringcsetcALTV2lem8  45274  funcringcsetclem8ALTV  45297  mapsnop  45353  fprmappr  45354  zlmodzxzel  45364  snlindsntorlem  45484  refdivmptf  45561  refdivmptfv  45565  elbigolo1  45576  2arymaptfo  45673  prelrrx2  45732  line2  45771  line2x  45773  line2y  45774  amgmwlem  46177