Theorem fssd 6725

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3899  ⟶wf 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ss 3916  df-f 6541

This theorem is used by:  fconst6g  6769  f1ounsn  7278  fsnex  7289  tposf2  8260  mapsnd  8907  mapss  8910  ralxpmap  8917  ac6sfi  9268  infpwfien  10134  infmap2  10288  cofsmo  10340  fin23lem32  10415  axdc3lem4  10524  pwfseqlem4a  10739  fseq1p1m1  13725  seqf1olem2  14178  wrdlen2i  15086  supcvg  16018  vdwlem8  17159  isacs2  17820  funcres2b  18065  funcestrcsetclem8  18314  funcsetcestrclem8  18329  gsumress  18864  gsumwsubmcl  19026  gsumws1  19027  pj1ghm  19910  gsumval3eu  20111  gsumval3  20114  gsumsubmcl  20126  gsumzadd  20129  gsumzoppg  20151  dprdsn  20245  pwssplit1  21327  pjdm2  22010  evlsvvval  22395  psdmul  22480  mat1dimelbas  22779  cnrest2  23597  cnprest2  23601  1stcelcls  23773  xkoptsub  23966  tsmssubm  24455  cncfss  25213  ipcn  25560  equivcau  25614  lmcau  25627  rrx0el  25712  i1fmulclem  26016  i1fres  26019  mbfi1fseqlem4  26032  itg2mulclem  26060  limccnp  26204  dvcmulf  26258  dvcobr  26259  dvcnvlem  26289  dvcnv  26290  dvef  26293  elply2  26507  plyeq0lem  26522  plyaddlem  26527  plymullem  26528  dgrlem  26541  coeidlem  26549  jensenlem2  27308  jensen  27309  om2noseqlt  28678  om2noseqlt2  28679  om2noseqf1o  28680  umgrupgr  29674  upgr1e  29684  umgrislfupgr  29694  usgrislfuspgr  29761  upgrres1  29887  umgrres1  29888  umgr2v2e  30099  0clwlkv  30715  minvecolem3  31471  minvecolem4  31475  occllem  31898  chscllem2  32233  chscllem4  32235  pjhf  32303  elrgspnsubrunlem1  33801  gsumind  33899  islinds5  33916  ellspds  33917  linds2eq  33929  1arithidomlem2  34061  1arithidom  34062  dfufd2lem  34074  selvply1rhmlemb  34144  mplmulmvr  34164  psrmonprod  34177  mplgsum  34178  esplyfval0  34189  esplylem  34191  esplympl  34192  esplyfv1  34194  esplyfval3  34197  esplyfval1  34198  esplyfvaln  34199  esplyind  34200  fedgmullem1  34254  fedgmullem2  34255  locfinref  34466  esumsnf  34689  hashreprin  35242  poimirlem29  38547  dochpolN  42527  aks6d1c7lem1  43210  evlsbagval  43594  evlsmhpvvval  43603  mhphf  43605  ismrc  43691  mapfzcons  43706  pwssplit4  44075  ntrf2  45109  binomcxplemnn0  45318  fcomptss  46186  fcoss  46192  frexr  46365  climreeq  46594  limccog  46601  limcrecl  46610  limsupre  46620  liminflimsupclim  46786  cncficcgt0  46867  dvdivcncf  46906  dvbdfbdioolem1  46907  ioodvbdlimc1lem1  46910  ioodvbdlimc1lem2  46911  ioodvbdlimc1  46912  ioodvbdlimc2lem  46913  ioodvbdlimc2  46914  dvnprodlem2  46926  voliooicof  46975  volicofmpt  46976  stoweidlem39  47018  stoweidlem59  47038  dirkercncflem3  47084  dirkercncf  47086  fourierdlem48  47133  fourierdlem49  47134  fourierdlem50  47135  fourierdlem51  47136  fourierdlem52  47137  fourierdlem54  47139  fourierdlem59  47144  fourierdlem70  47155  fourierdlem72  47157  fourierdlem73  47158  fourierdlem74  47159  fourierdlem75  47160  fourierdlem76  47161  fourierdlem79  47164  fourierdlem84  47169  fourierdlem85  47170  fourierdlem88  47173  fourierdlem93  47178  fourierdlem94  47179  fourierdlem96  47181  fourierdlem97  47182  fourierdlem98  47183  fourierdlem99  47184  fourierdlem102  47187  fourierdlem103  47188  fourierdlem104  47189  fourierdlem111  47196  fourierdlem112  47197  fourierdlem113  47198  fourierdlem114  47199  fouriercn  47211  elaa2lem  47212  rrxtopnfi  47266  rrndistlt  47269  ioorrnopnlem  47283  issalnnd  47324  fge0icoicc  47344  fge0iccre  47353  sge0isum  47406  sge0gtfsumgt  47422  sge0seq  47425  ismeannd  47446  meaiuninclem  47459  caragenunicl  47503  caratheodorylem1  47505  caratheodorylem2  47506  isomenndlem  47509  elhoi  47521  sge0hsphoire  47568  hoidmv1le  47573  hoiqssbllem3  47603  hspmbllem2  47606  ovolval2lem  47622  ovolval3  47626  ovolval4lem2  47629  ovolval5lem2  47632  ovnovollem1  47635  ovnovollem2  47636  iunhoiioolem  47654  iccvonmbllem  47657  vonioolem2  47660  vonioo  47661  smfco  47781  nnsum3primesgbe  48859  nnsum4primesodd  48863  nnsum4primesoddALTV  48864  grimuhgr  48954  uhgrimisgrgric  48998  isubgr3stgrlem6  49038  1hegrlfgr  49199  funcringcsetcALTV2lem8  49363  funcringcsetclem8ALTV  49386  mapsnop  49425  fprmappr  49426  zlmodzxzel  49436  snlindsntorlem  49551  refdivmptf  49623  refdivmptfv  49627  elbigolo1  49638  2arymaptfo  49735  prelrrx2  49794  line2  49833  line2x  49835  line2y  49836  amgmwlem  50956