Theorem fssd 6679

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

Syntax hints:   → wi 4   ⊆ wss 3890  ⟶wf 6488

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3907  df-f 6496

This theorem is referenced by:  fconst6g  6723  f1ounsn  7220  fsnex  7231  tposf2  8193  mapsnd  8827  mapss  8830  ralxpmap  8837  ac6sfi  9187  infpwfien  9975  infmap2  10130  cofsmo  10182  fin23lem32  10257  axdc3lem4  10366  pwfseqlem4a  10575  fseq1p1m1  13543  seqf1olem2  13995  wrdlen2i  14895  supcvg  15812  vdwlem8  16950  isacs2  17610  funcres2b  17855  funcestrcsetclem8  18104  funcsetcestrclem8  18119  gsumress  18641  gsumwsubmcl  18796  gsumws1  18797  pj1ghm  19669  gsumval3eu  19870  gsumval3  19873  gsumsubmcl  19885  gsumzadd  19888  gsumzoppg  19910  dprdsn  20004  pwssplit1  21046  pjdm2  21701  evlsvvval  22081  psdmul  22142  mat1dimelbas  22446  cnrest2  23261  cnprest2  23265  1stcelcls  23436  xkoptsub  23629  tsmssubm  24118  cncfss  24876  ipcn  25223  equivcau  25277  lmcau  25290  rrx0el  25375  i1fmulclem  25679  i1fres  25682  mbfi1fseqlem4  25695  itg2mulclem  25723  limccnp  25868  dvcmulf  25922  dvcobr  25923  dvcnvlem  25953  dvcnv  25954  dvef  25957  elply2  26171  plyeq0lem  26185  plyaddlem  26190  plymullem  26191  dgrlem  26204  coeidlem  26212  jensenlem2  26965  jensen  26966  om2noseqlt  28305  om2noseqlt2  28306  om2noseqf1o  28307  umgrupgr  29186  upgr1e  29196  umgrislfupgr  29206  usgrislfuspgr  29270  upgrres1  29396  umgrres1  29397  umgr2v2e  29609  0clwlkv  30216  minvecolem3  30962  minvecolem4  30966  occllem  31389  chscllem2  31724  chscllem4  31726  pjhf  31794  elrgspnsubrunlem1  33323  gsumind  33420  islinds5  33442  ellspds  33443  linds2eq  33456  1arithidomlem2  33611  1arithidom  33612  dfufd2lem  33624  mplmulmvr  33698  psrmonprod  33711  mplgsum  33712  esplyfval0  33723  esplylem  33725  esplympl  33726  esplyfv1  33728  esplyfval3  33731  esplyfval1  33732  esplyfvaln  33733  esplyind  33734  fedgmullem1  33789  fedgmullem2  33790  locfinref  34001  esumsnf  34224  hashreprin  34780  poimirlem29  37984  dochpolN  41950  aks6d1c7lem1  42633  evlsbagval  43016  evlsmhpvvval  43042  mhphf  43044  ismrc  43147  mapfzcons  43162  pwssplit4  43535  ntrf2  44569  binomcxplemnn0  44794  fcomptss  45650  fcoss  45657  frexr  45832  climreeq  46061  limccog  46068  limcrecl  46077  limsupre  46087  liminflimsupclim  46253  cncficcgt0  46334  dvdivcncf  46373  dvbdfbdioolem1  46374  ioodvbdlimc1lem1  46377  ioodvbdlimc1lem2  46378  ioodvbdlimc1  46379  ioodvbdlimc2lem  46380  ioodvbdlimc2  46381  dvnprodlem2  46393  voliooicof  46442  volicofmpt  46443  stoweidlem39  46485  stoweidlem59  46505  dirkercncflem3  46551  dirkercncf  46553  fourierdlem48  46600  fourierdlem49  46601  fourierdlem50  46602  fourierdlem51  46603  fourierdlem52  46604  fourierdlem54  46606  fourierdlem59  46611  fourierdlem70  46622  fourierdlem72  46624  fourierdlem73  46625  fourierdlem74  46626  fourierdlem75  46627  fourierdlem76  46628  fourierdlem79  46631  fourierdlem84  46636  fourierdlem85  46637  fourierdlem88  46640  fourierdlem93  46645  fourierdlem94  46646  fourierdlem96  46648  fourierdlem97  46649  fourierdlem98  46650  fourierdlem99  46651  fourierdlem102  46654  fourierdlem103  46655  fourierdlem104  46656  fourierdlem111  46663  fourierdlem112  46664  fourierdlem113  46665  fourierdlem114  46666  fouriercn  46678  elaa2lem  46679  rrxtopnfi  46733  rrndistlt  46736  ioorrnopnlem  46750  issalnnd  46791  fge0icoicc  46811  fge0iccre  46820  sge0isum  46873  sge0gtfsumgt  46889  sge0seq  46892  ismeannd  46913  meaiuninclem  46926  caragenunicl  46970  caratheodorylem1  46972  caratheodorylem2  46973  isomenndlem  46976  elhoi  46988  sge0hsphoire  47035  hoidmv1le  47040  hoiqssbllem3  47070  hspmbllem2  47073  ovolval2lem  47089  ovolval3  47093  ovolval4lem2  47096  ovolval5lem2  47099  ovnovollem1  47102  ovnovollem2  47103  iunhoiioolem  47121  iccvonmbllem  47124  vonioolem2  47127  vonioo  47128  smfco  47248  nnsum3primesgbe  48280  nnsum4primesodd  48284  nnsum4primesoddALTV  48285  grimuhgr  48375  uhgrimisgrgric  48419  isubgr3stgrlem6  48459  1hegrlfgr  48620  funcringcsetcALTV2lem8  48785  funcringcsetclem8ALTV  48808  mapsnop  48832  fprmappr  48833  zlmodzxzel  48843  snlindsntorlem  48958  refdivmptf  49030  refdivmptfv  49034  elbigolo1  49045  2arymaptfo  49142  prelrrx2  49201  line2  49240  line2x  49242  line2y  49243  amgmwlem  50289