Theorem fssd 6753

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

Syntax hints:   → wi 4   ⊆ wss 3962  ⟶wf 6558

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3979  df-f 6566

This theorem is referenced by:  fconst6g  6797  f1ounsn  7291  fsnex  7302  tposf2  8273  mapsnd  8924  mapss  8927  ralxpmap  8934  ac6sfi  9317  infpwfien  10099  infmap2  10254  cofsmo  10306  fin23lem32  10381  axdc3lem4  10490  pwfseqlem4a  10698  fseq1p1m1  13634  seqf1olem2  14079  wrdlen2i  14977  supcvg  15888  vdwlem8  17021  isacs2  17697  funcres2b  17947  funcestrcsetclem8  18202  funcsetcestrclem8  18217  gsumress  18707  gsumwsubmcl  18862  gsumws1  18863  pj1ghm  19735  gsumval3eu  19936  gsumval3  19939  gsumsubmcl  19951  gsumzadd  19954  gsumzoppg  19976  dprdsn  20070  pwssplit1  21075  pjdm2  21748  psdmul  22187  mat1dimelbas  22492  cnrest2  23309  cnprest2  23313  1stcelcls  23484  xkoptsub  23677  tsmssubm  24166  cncfss  24938  ipcn  25293  equivcau  25347  lmcau  25360  rrx0el  25445  i1fmulclem  25751  i1fres  25754  mbfi1fseqlem4  25767  itg2mulclem  25795  limccnp  25940  dvcmulf  25996  dvcobr  25997  dvcobrOLD  25998  dvcnvlem  26028  dvcnv  26029  dvef  26032  elply2  26249  plyeq0lem  26263  plyaddlem  26268  plymullem  26269  dgrlem  26282  coeidlem  26290  jensenlem2  27045  jensen  27046  om2noseqlt  28319  om2noseqlt2  28320  om2noseqf1o  28321  umgrupgr  29134  upgr1e  29144  umgrislfupgr  29154  usgrislfuspgr  29218  upgrres1  29344  umgrres1  29345  umgr2v2e  29557  0clwlkv  30159  minvecolem3  30904  minvecolem4  30908  occllem  31331  chscllem2  31666  chscllem4  31668  pjhf  31736  islinds5  33374  ellspds  33375  linds2eq  33388  1arithidomlem2  33543  1arithidom  33544  dfufd2lem  33556  fedgmullem1  33656  fedgmullem2  33657  locfinref  33801  esumsnf  34044  hashreprin  34613  poimirlem29  37635  dochpolN  41472  aks6d1c7lem1  42161  evlsvvval  42549  evlsbagval  42552  evlsmhpvvval  42581  mhphf  42583  ismrc  42688  mapfzcons  42703  pwssplit4  43077  ntrf2  44113  binomcxplemnn0  44344  fcomptss  45145  fcoss  45152  frexr  45334  climreeq  45568  limccog  45575  limcrecl  45584  limsupre  45596  liminflimsupclim  45762  cncficcgt0  45843  dvdivcncf  45882  dvbdfbdioolem1  45883  ioodvbdlimc1lem1  45886  ioodvbdlimc1lem2  45887  ioodvbdlimc1  45888  ioodvbdlimc2lem  45889  ioodvbdlimc2  45890  dvnprodlem2  45902  voliooicof  45951  volicofmpt  45952  stoweidlem39  45994  stoweidlem59  46014  dirkercncflem3  46060  dirkercncf  46062  fourierdlem48  46109  fourierdlem49  46110  fourierdlem50  46111  fourierdlem51  46112  fourierdlem52  46113  fourierdlem54  46115  fourierdlem59  46120  fourierdlem70  46131  fourierdlem72  46133  fourierdlem73  46134  fourierdlem74  46135  fourierdlem75  46136  fourierdlem76  46137  fourierdlem79  46140  fourierdlem84  46145  fourierdlem85  46146  fourierdlem88  46149  fourierdlem93  46154  fourierdlem94  46155  fourierdlem96  46157  fourierdlem97  46158  fourierdlem98  46159  fourierdlem99  46160  fourierdlem102  46163  fourierdlem103  46164  fourierdlem104  46165  fourierdlem111  46172  fourierdlem112  46173  fourierdlem113  46174  fourierdlem114  46175  fouriercn  46187  elaa2lem  46188  rrxtopnfi  46242  rrndistlt  46245  ioorrnopnlem  46259  issalnnd  46300  fge0icoicc  46320  fge0iccre  46329  sge0isum  46382  sge0gtfsumgt  46398  sge0seq  46401  ismeannd  46422  meaiuninclem  46435  caragenunicl  46479  caratheodorylem1  46481  caratheodorylem2  46482  isomenndlem  46485  elhoi  46497  hoicvr  46503  sge0hsphoire  46544  hoidmv1le  46549  hoiqssbllem3  46579  hspmbllem2  46582  ovolval2lem  46598  ovolval3  46602  ovolval4lem2  46605  ovolval5lem2  46608  ovnovollem1  46611  ovnovollem2  46612  iunhoiioolem  46630  iccvonmbllem  46633  vonioolem2  46636  vonioo  46637  smfco  46757  nnsum3primesgbe  47716  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  grimuhgr  47815  uhgrimisgrgric  47836  isubgr3stgrlem6  47873  1hegrlfgr  47975  funcringcsetcALTV2lem8  48140  funcringcsetclem8ALTV  48163  mapsnop  48188  fprmappr  48189  zlmodzxzel  48199  snlindsntorlem  48315  refdivmptf  48391  refdivmptfv  48395  elbigolo1  48406  2arymaptfo  48503  prelrrx2  48562  line2  48601  line2x  48603  line2y  48604  amgmwlem  49032