Theorem fssd 6723

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

Syntax hints:   → wi 4   ⊆ wss 3905  ⟶wf 6532

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ss 3922  df-f 6540

This theorem is referenced by:  fconst6g  6767  f1ounsn  7270  fsnex  7281  tposf2  8242  mapsnd  8880  mapss  8883  ralxpmap  8890  ac6sfi  9240  infpwfien  10042  infmap2  10196  cofsmo  10248  fin23lem32  10323  axdc3lem4  10432  pwfseqlem4a  10641  fseq1p1m1  13622  seqf1olem2  14074  wrdlen2i  14975  supcvg  15906  vdwlem8  17043  isacs2  17704  funcres2b  17949  funcestrcsetclem8  18198  funcsetcestrclem8  18213  gsumress  18735  gsumwsubmcl  18891  gsumws1  18892  pj1ghm  19768  gsumval3eu  19969  gsumval3  19972  gsumsubmcl  19984  gsumzadd  19987  gsumzoppg  20009  dprdsn  20103  pwssplit1  21180  pjdm2  21861  evlsvvval  22244  psdmul  22329  mat1dimelbas  22628  cnrest2  23443  cnprest2  23447  1stcelcls  23618  xkoptsub  23811  tsmssubm  24300  cncfss  25058  ipcn  25405  equivcau  25459  lmcau  25472  rrx0el  25557  i1fmulclem  25861  i1fres  25864  mbfi1fseqlem4  25877  itg2mulclem  25905  limccnp  26050  dvcmulf  26104  dvcobr  26105  dvcnvlem  26135  dvcnv  26136  dvef  26139  elply2  26353  plyeq0lem  26367  plyaddlem  26372  plymullem  26373  dgrlem  26386  coeidlem  26394  jensenlem2  27152  jensen  27153  om2noseqlt  28492  om2noseqlt2  28493  om2noseqf1o  28494  umgrupgr  29453  upgr1e  29463  umgrislfupgr  29473  usgrislfuspgr  29537  upgrres1  29663  umgrres1  29664  umgr2v2e  29875  0clwlkv  30482  minvecolem3  31228  minvecolem4  31232  occllem  31655  chscllem2  31990  chscllem4  31992  pjhf  32060  elrgspnsubrunlem1  33567  gsumind  33665  islinds5  33682  ellspds  33683  linds2eq  33694  1arithidomlem2  33826  1arithidom  33827  dfufd2lem  33839  selvply1rhmlemb  33909  mplmulmvr  33929  psrmonprod  33942  mplgsum  33943  esplyfval0  33954  esplylem  33956  esplympl  33957  esplyfv1  33959  esplyfval3  33962  esplyfval1  33963  esplyfvaln  33964  esplyind  33965  fedgmullem1  34019  fedgmullem2  34020  locfinref  34231  esumsnf  34454  hashreprin  35007  poimirlem29  38300  dochpolN  42264  aks6d1c7lem1  42947  evlsbagval  43318  evlsmhpvvval  43327  mhphf  43329  ismrc  43432  mapfzcons  43447  pwssplit4  43816  ntrf2  44850  binomcxplemnn0  45059  fcomptss  45920  fcoss  45926  frexr  46100  climreeq  46329  limccog  46336  limcrecl  46345  limsupre  46355  liminflimsupclim  46521  cncficcgt0  46602  dvdivcncf  46641  dvbdfbdioolem1  46642  ioodvbdlimc1lem1  46645  ioodvbdlimc1lem2  46646  ioodvbdlimc1  46647  ioodvbdlimc2lem  46648  ioodvbdlimc2  46649  dvnprodlem2  46661  voliooicof  46710  volicofmpt  46711  stoweidlem39  46753  stoweidlem59  46773  dirkercncflem3  46819  dirkercncf  46821  fourierdlem48  46868  fourierdlem49  46869  fourierdlem50  46870  fourierdlem51  46871  fourierdlem52  46872  fourierdlem54  46874  fourierdlem59  46879  fourierdlem70  46890  fourierdlem72  46892  fourierdlem73  46893  fourierdlem74  46894  fourierdlem75  46895  fourierdlem76  46896  fourierdlem79  46899  fourierdlem84  46904  fourierdlem85  46905  fourierdlem88  46908  fourierdlem93  46913  fourierdlem94  46914  fourierdlem96  46916  fourierdlem97  46917  fourierdlem98  46918  fourierdlem99  46919  fourierdlem102  46922  fourierdlem103  46923  fourierdlem104  46924  fourierdlem111  46931  fourierdlem112  46932  fourierdlem113  46933  fourierdlem114  46934  fouriercn  46946  elaa2lem  46947  rrxtopnfi  47001  rrndistlt  47004  ioorrnopnlem  47018  issalnnd  47059  fge0icoicc  47079  fge0iccre  47088  sge0isum  47141  sge0gtfsumgt  47157  sge0seq  47160  ismeannd  47181  meaiuninclem  47194  caragenunicl  47238  caratheodorylem1  47240  caratheodorylem2  47241  isomenndlem  47244  elhoi  47256  sge0hsphoire  47303  hoidmv1le  47308  hoiqssbllem3  47338  hspmbllem2  47341  ovolval2lem  47357  ovolval3  47361  ovolval4lem2  47364  ovolval5lem2  47367  ovnovollem1  47370  ovnovollem2  47371  iunhoiioolem  47389  iccvonmbllem  47392  vonioolem2  47395  vonioo  47396  smfco  47516  nnsum3primesgbe  48557  nnsum4primesodd  48561  nnsum4primesoddALTV  48562  grimuhgr  48652  uhgrimisgrgric  48696  isubgr3stgrlem6  48736  1hegrlfgr  48897  funcringcsetcALTV2lem8  49062  funcringcsetclem8ALTV  49085  mapsnop  49124  fprmappr  49125  zlmodzxzel  49135  snlindsntorlem  49250  refdivmptf  49322  refdivmptfv  49326  elbigolo1  49337  2arymaptfo  49434  prelrrx2  49493  line2  49532  line2x  49534  line2y  49535  amgmwlem  50622