Theorem fssd 6669

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

Syntax hints:   → wi 4   ⊆ wss 3903  ⟶wf 6478

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3920  df-f 6486

This theorem is referenced by:  fconst6g  6713  f1ounsn  7209  fsnex  7220  tposf2  8183  mapsnd  8813  mapss  8816  ralxpmap  8823  ac6sfi  9173  infpwfien  9956  infmap2  10111  cofsmo  10163  fin23lem32  10238  axdc3lem4  10347  pwfseqlem4a  10555  fseq1p1m1  13501  seqf1olem2  13949  wrdlen2i  14849  supcvg  15763  vdwlem8  16900  isacs2  17559  funcres2b  17804  funcestrcsetclem8  18053  funcsetcestrclem8  18068  gsumress  18556  gsumwsubmcl  18711  gsumws1  18712  pj1ghm  19582  gsumval3eu  19783  gsumval3  19786  gsumsubmcl  19798  gsumzadd  19801  gsumzoppg  19823  dprdsn  19917  pwssplit1  20963  pjdm2  21618  psdmul  22051  mat1dimelbas  22356  cnrest2  23171  cnprest2  23175  1stcelcls  23346  xkoptsub  23539  tsmssubm  24028  cncfss  24790  ipcn  25144  equivcau  25198  lmcau  25211  rrx0el  25296  i1fmulclem  25601  i1fres  25604  mbfi1fseqlem4  25617  itg2mulclem  25645  limccnp  25790  dvcmulf  25846  dvcobr  25847  dvcobrOLD  25848  dvcnvlem  25878  dvcnv  25879  dvef  25882  elply2  26099  plyeq0lem  26113  plyaddlem  26118  plymullem  26119  dgrlem  26132  coeidlem  26140  jensenlem2  26896  jensen  26897  om2noseqlt  28198  om2noseqlt2  28199  om2noseqf1o  28200  umgrupgr  29048  upgr1e  29058  umgrislfupgr  29068  usgrislfuspgr  29132  upgrres1  29258  umgrres1  29259  umgr2v2e  29471  0clwlkv  30075  minvecolem3  30820  minvecolem4  30824  occllem  31247  chscllem2  31582  chscllem4  31584  pjhf  31652  elrgspnsubrunlem1  33187  islinds5  33304  ellspds  33305  linds2eq  33318  1arithidomlem2  33473  1arithidom  33474  dfufd2lem  33486  fedgmullem1  33596  fedgmullem2  33597  locfinref  33808  esumsnf  34031  hashreprin  34588  poimirlem29  37629  dochpolN  41469  aks6d1c7lem1  42153  evlsvvval  42536  evlsbagval  42539  evlsmhpvvval  42568  mhphf  42570  ismrc  42674  mapfzcons  42689  pwssplit4  43062  ntrf2  44097  binomcxplemnn0  44322  fcomptss  45181  fcoss  45188  frexr  45364  climreeq  45594  limccog  45601  limcrecl  45610  limsupre  45622  liminflimsupclim  45788  cncficcgt0  45869  dvdivcncf  45908  dvbdfbdioolem1  45909  ioodvbdlimc1lem1  45912  ioodvbdlimc1lem2  45913  ioodvbdlimc1  45914  ioodvbdlimc2lem  45915  ioodvbdlimc2  45916  dvnprodlem2  45928  voliooicof  45977  volicofmpt  45978  stoweidlem39  46020  stoweidlem59  46040  dirkercncflem3  46086  dirkercncf  46088  fourierdlem48  46135  fourierdlem49  46136  fourierdlem50  46137  fourierdlem51  46138  fourierdlem52  46139  fourierdlem54  46141  fourierdlem59  46146  fourierdlem70  46157  fourierdlem72  46159  fourierdlem73  46160  fourierdlem74  46161  fourierdlem75  46162  fourierdlem76  46163  fourierdlem79  46166  fourierdlem84  46171  fourierdlem85  46172  fourierdlem88  46175  fourierdlem93  46180  fourierdlem94  46181  fourierdlem96  46183  fourierdlem97  46184  fourierdlem98  46185  fourierdlem99  46186  fourierdlem102  46189  fourierdlem103  46190  fourierdlem104  46191  fourierdlem111  46198  fourierdlem112  46199  fourierdlem113  46200  fourierdlem114  46201  fouriercn  46213  elaa2lem  46214  rrxtopnfi  46268  rrndistlt  46271  ioorrnopnlem  46285  issalnnd  46326  fge0icoicc  46346  fge0iccre  46355  sge0isum  46408  sge0gtfsumgt  46424  sge0seq  46427  ismeannd  46448  meaiuninclem  46461  caragenunicl  46505  caratheodorylem1  46507  caratheodorylem2  46508  isomenndlem  46511  elhoi  46523  hoicvr  46529  sge0hsphoire  46570  hoidmv1le  46575  hoiqssbllem3  46605  hspmbllem2  46608  ovolval2lem  46624  ovolval3  46628  ovolval4lem2  46631  ovolval5lem2  46634  ovnovollem1  46637  ovnovollem2  46638  iunhoiioolem  46656  iccvonmbllem  46659  vonioolem2  46662  vonioo  46663  smfco  46783  nnsum3primesgbe  47776  nnsum4primesodd  47780  nnsum4primesoddALTV  47781  grimuhgr  47871  uhgrimisgrgric  47915  isubgr3stgrlem6  47955  1hegrlfgr  48116  funcringcsetcALTV2lem8  48281  funcringcsetclem8ALTV  48304  mapsnop  48328  fprmappr  48329  zlmodzxzel  48339  snlindsntorlem  48455  refdivmptf  48527  refdivmptfv  48531  elbigolo1  48542  2arymaptfo  48639  prelrrx2  48698  line2  48737  line2x  48739  line2y  48740  amgmwlem  49787