Theorem fssd 6663

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

Syntax hints:   → wi 4   ⊆ wss 3897  ⟶wf 6472

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3914  df-f 6480

This theorem is referenced by:  fconst6g  6707  f1ounsn  7201  fsnex  7212  tposf2  8175  mapsnd  8805  mapss  8808  ralxpmap  8815  ac6sfi  9163  infpwfien  9948  infmap2  10103  cofsmo  10155  fin23lem32  10230  axdc3lem4  10339  pwfseqlem4a  10547  fseq1p1m1  13493  seqf1olem2  13944  wrdlen2i  14844  supcvg  15758  vdwlem8  16895  isacs2  17554  funcres2b  17799  funcestrcsetclem8  18048  funcsetcestrclem8  18063  gsumress  18585  gsumwsubmcl  18740  gsumws1  18741  pj1ghm  19610  gsumval3eu  19811  gsumval3  19814  gsumsubmcl  19826  gsumzadd  19829  gsumzoppg  19851  dprdsn  19945  pwssplit1  20988  pjdm2  21643  psdmul  22076  mat1dimelbas  22381  cnrest2  23196  cnprest2  23200  1stcelcls  23371  xkoptsub  23564  tsmssubm  24053  cncfss  24814  ipcn  25168  equivcau  25222  lmcau  25235  rrx0el  25320  i1fmulclem  25625  i1fres  25628  mbfi1fseqlem4  25641  itg2mulclem  25669  limccnp  25814  dvcmulf  25870  dvcobr  25871  dvcobrOLD  25872  dvcnvlem  25902  dvcnv  25903  dvef  25906  elply2  26123  plyeq0lem  26137  plyaddlem  26142  plymullem  26143  dgrlem  26156  coeidlem  26164  jensenlem2  26920  jensen  26921  om2noseqlt  28224  om2noseqlt2  28225  om2noseqf1o  28226  umgrupgr  29076  upgr1e  29086  umgrislfupgr  29096  usgrislfuspgr  29160  upgrres1  29286  umgrres1  29287  umgr2v2e  29499  0clwlkv  30103  minvecolem3  30848  minvecolem4  30852  occllem  31275  chscllem2  31610  chscllem4  31612  pjhf  31680  elrgspnsubrunlem1  33206  gsumind  33302  islinds5  33324  ellspds  33325  linds2eq  33338  1arithidomlem2  33493  1arithidom  33494  dfufd2lem  33506  esplylem  33579  esplympl  33580  esplyfv1  33582  fedgmullem1  33634  fedgmullem2  33635  locfinref  33846  esumsnf  34069  hashreprin  34625  poimirlem29  37689  dochpolN  41529  aks6d1c7lem1  42213  evlsvvval  42596  evlsbagval  42599  evlsmhpvvval  42628  mhphf  42630  ismrc  42734  mapfzcons  42749  pwssplit4  43122  ntrf2  44157  binomcxplemnn0  44382  fcomptss  45240  fcoss  45247  frexr  45423  climreeq  45653  limccog  45660  limcrecl  45669  limsupre  45679  liminflimsupclim  45845  cncficcgt0  45926  dvdivcncf  45965  dvbdfbdioolem1  45966  ioodvbdlimc1lem1  45969  ioodvbdlimc1lem2  45970  ioodvbdlimc1  45971  ioodvbdlimc2lem  45972  ioodvbdlimc2  45973  dvnprodlem2  45985  voliooicof  46034  volicofmpt  46035  stoweidlem39  46077  stoweidlem59  46097  dirkercncflem3  46143  dirkercncf  46145  fourierdlem48  46192  fourierdlem49  46193  fourierdlem50  46194  fourierdlem51  46195  fourierdlem52  46196  fourierdlem54  46198  fourierdlem59  46203  fourierdlem70  46214  fourierdlem72  46216  fourierdlem73  46217  fourierdlem74  46218  fourierdlem75  46219  fourierdlem76  46220  fourierdlem79  46223  fourierdlem84  46228  fourierdlem85  46229  fourierdlem88  46232  fourierdlem93  46237  fourierdlem94  46238  fourierdlem96  46240  fourierdlem97  46241  fourierdlem98  46242  fourierdlem99  46243  fourierdlem102  46246  fourierdlem103  46247  fourierdlem104  46248  fourierdlem111  46255  fourierdlem112  46256  fourierdlem113  46257  fourierdlem114  46258  fouriercn  46270  elaa2lem  46271  rrxtopnfi  46325  rrndistlt  46328  ioorrnopnlem  46342  issalnnd  46383  fge0icoicc  46403  fge0iccre  46412  sge0isum  46465  sge0gtfsumgt  46481  sge0seq  46484  ismeannd  46505  meaiuninclem  46518  caragenunicl  46562  caratheodorylem1  46564  caratheodorylem2  46565  isomenndlem  46568  elhoi  46580  hoicvr  46586  sge0hsphoire  46627  hoidmv1le  46632  hoiqssbllem3  46662  hspmbllem2  46665  ovolval2lem  46681  ovolval3  46685  ovolval4lem2  46688  ovolval5lem2  46691  ovnovollem1  46694  ovnovollem2  46695  iunhoiioolem  46713  iccvonmbllem  46716  vonioolem2  46719  vonioo  46720  smfco  46840  nnsum3primesgbe  47823  nnsum4primesodd  47827  nnsum4primesoddALTV  47828  grimuhgr  47918  uhgrimisgrgric  47962  isubgr3stgrlem6  48002  1hegrlfgr  48163  funcringcsetcALTV2lem8  48328  funcringcsetclem8ALTV  48351  mapsnop  48375  fprmappr  48376  zlmodzxzel  48386  snlindsntorlem  48502  refdivmptf  48574  refdivmptfv  48578  elbigolo1  48589  2arymaptfo  48686  prelrrx2  48745  line2  48784  line2x  48786  line2y  48787  amgmwlem  49834