Theorem fssd 6705

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

Syntax hints:   → wi 4   ⊆ wss 3914  ⟶wf 6507

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 3931  df-f 6515

This theorem is referenced by:  fconst6g  6749  f1ounsn  7247  fsnex  7258  tposf2  8229  mapsnd  8859  mapss  8862  ralxpmap  8869  ac6sfi  9231  infpwfien  10015  infmap2  10170  cofsmo  10222  fin23lem32  10297  axdc3lem4  10406  pwfseqlem4a  10614  fseq1p1m1  13559  seqf1olem2  14007  wrdlen2i  14908  supcvg  15822  vdwlem8  16959  isacs2  17614  funcres2b  17859  funcestrcsetclem8  18108  funcsetcestrclem8  18123  gsumress  18609  gsumwsubmcl  18764  gsumws1  18765  pj1ghm  19633  gsumval3eu  19834  gsumval3  19837  gsumsubmcl  19849  gsumzadd  19852  gsumzoppg  19874  dprdsn  19968  pwssplit1  20966  pjdm2  21620  psdmul  22053  mat1dimelbas  22358  cnrest2  23173  cnprest2  23177  1stcelcls  23348  xkoptsub  23541  tsmssubm  24030  cncfss  24792  ipcn  25146  equivcau  25200  lmcau  25213  rrx0el  25298  i1fmulclem  25603  i1fres  25606  mbfi1fseqlem4  25619  itg2mulclem  25647  limccnp  25792  dvcmulf  25848  dvcobr  25849  dvcobrOLD  25850  dvcnvlem  25880  dvcnv  25881  dvef  25884  elply2  26101  plyeq0lem  26115  plyaddlem  26120  plymullem  26121  dgrlem  26134  coeidlem  26142  jensenlem2  26898  jensen  26899  om2noseqlt  28193  om2noseqlt2  28194  om2noseqf1o  28195  umgrupgr  29030  upgr1e  29040  umgrislfupgr  29050  usgrislfuspgr  29114  upgrres1  29240  umgrres1  29241  umgr2v2e  29453  0clwlkv  30060  minvecolem3  30805  minvecolem4  30809  occllem  31232  chscllem2  31567  chscllem4  31569  pjhf  31637  elrgspnsubrunlem1  33198  islinds5  33338  ellspds  33339  linds2eq  33352  1arithidomlem2  33507  1arithidom  33508  dfufd2lem  33520  fedgmullem1  33625  fedgmullem2  33626  locfinref  33831  esumsnf  34054  hashreprin  34611  poimirlem29  37643  dochpolN  41484  aks6d1c7lem1  42168  evlsvvval  42551  evlsbagval  42554  evlsmhpvvval  42583  mhphf  42585  ismrc  42689  mapfzcons  42704  pwssplit4  43078  ntrf2  44113  binomcxplemnn0  44338  fcomptss  45197  fcoss  45204  frexr  45381  climreeq  45611  limccog  45618  limcrecl  45627  limsupre  45639  liminflimsupclim  45805  cncficcgt0  45886  dvdivcncf  45925  dvbdfbdioolem1  45926  ioodvbdlimc1lem1  45929  ioodvbdlimc1lem2  45930  ioodvbdlimc1  45931  ioodvbdlimc2lem  45932  ioodvbdlimc2  45933  dvnprodlem2  45945  voliooicof  45994  volicofmpt  45995  stoweidlem39  46037  stoweidlem59  46057  dirkercncflem3  46103  dirkercncf  46105  fourierdlem48  46152  fourierdlem49  46153  fourierdlem50  46154  fourierdlem51  46155  fourierdlem52  46156  fourierdlem54  46158  fourierdlem59  46163  fourierdlem70  46174  fourierdlem72  46176  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem79  46183  fourierdlem84  46188  fourierdlem85  46189  fourierdlem88  46192  fourierdlem93  46197  fourierdlem94  46198  fourierdlem96  46200  fourierdlem97  46201  fourierdlem98  46202  fourierdlem99  46203  fourierdlem102  46206  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  fourierdlem112  46216  fourierdlem113  46217  fourierdlem114  46218  fouriercn  46230  elaa2lem  46231  rrxtopnfi  46285  rrndistlt  46288  ioorrnopnlem  46302  issalnnd  46343  fge0icoicc  46363  fge0iccre  46372  sge0isum  46425  sge0gtfsumgt  46441  sge0seq  46444  ismeannd  46465  meaiuninclem  46478  caragenunicl  46522  caratheodorylem1  46524  caratheodorylem2  46525  isomenndlem  46528  elhoi  46540  hoicvr  46546  sge0hsphoire  46587  hoidmv1le  46592  hoiqssbllem3  46622  hspmbllem2  46625  ovolval2lem  46641  ovolval3  46645  ovolval4lem2  46648  ovolval5lem2  46651  ovnovollem1  46654  ovnovollem2  46655  iunhoiioolem  46673  iccvonmbllem  46676  vonioolem2  46679  vonioo  46680  smfco  46800  nnsum3primesgbe  47793  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  grimuhgr  47887  uhgrimisgrgric  47931  isubgr3stgrlem6  47970  1hegrlfgr  48120  funcringcsetcALTV2lem8  48285  funcringcsetclem8ALTV  48308  mapsnop  48332  fprmappr  48333  zlmodzxzel  48343  snlindsntorlem  48459  refdivmptf  48531  refdivmptfv  48535  elbigolo1  48546  2arymaptfo  48643  prelrrx2  48702  line2  48741  line2x  48743  line2y  48744  amgmwlem  49791