Theorem fssd 6528

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

Syntax hints:   → wi 4   ⊆ wss 3936  ⟶wf 6351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952  df-f 6359

This theorem is referenced by:  fconst6g  6568  fsnex  7039  tposf2  7916  mapsnd  8450  mapss  8453  ralxpmap  8460  ac6sfi  8762  infpwfien  9488  infmap2  9640  cofsmo  9691  fin23lem32  9766  axdc3lem4  9875  pwfseqlem4a  10083  fseq1p1m1  12982  seqf1olem2  13411  wrdlen2i  14304  supcvg  15211  vdwlem8  16324  isacs2  16924  funcres2b  17167  funcestrcsetclem8  17397  funcsetcestrclem8  17412  gsumress  17892  gsumwsubmcl  18001  gsumws1  18002  pj1ghm  18829  gsumval3eu  19024  gsumval3  19027  gsumsubmcl  19039  gsumzadd  19042  gsumzoppg  19064  dprdsn  19158  pwssplit1  19831  pjdm2  20855  mat1dimelbas  21080  cnrest2  21894  cnprest2  21898  1stcelcls  22069  xkoptsub  22262  tsmssubm  22751  cncfss  23507  ipcn  23849  equivcau  23903  lmcau  23916  rrx0el  24001  i1fmulclem  24303  i1fres  24306  mbfi1fseqlem4  24319  itg2mulclem  24347  limccnp  24489  dvcmulf  24542  dvcobr  24543  dvcnvlem  24573  dvcnv  24574  dvef  24577  elply2  24786  plyeq0lem  24800  plyaddlem  24805  plymullem  24806  dgrlem  24819  coeidlem  24827  jensenlem2  25565  jensen  25566  umgrupgr  26888  upgr1e  26898  umgrislfupgr  26908  usgrislfuspgr  26969  upgrres1  27095  umgrres1  27096  umgr2v2e  27307  0clwlkv  27910  minvecolem3  28653  minvecolem4  28657  occllem  29080  chscllem2  29415  chscllem4  29417  pjhf  29485  islinds5  30932  ellspds  30933  linds2eq  30941  fedgmullem1  31025  fedgmullem2  31026  locfinref  31105  esumsnf  31323  hashreprin  31891  poimirlem29  34936  dochpolN  38641  ismrc  39347  mapfzcons  39362  pwssplit4  39738  ntrf2  40523  binomcxplemnn0  40730  fcomptss  41515  fcoss  41522  fco3  41540  frexr  41704  climreeq  41943  limccog  41950  limcrecl  41959  limsupre  41971  liminflimsupclim  42137  cncficcgt0  42220  dvdivcncf  42261  dvbdfbdioolem1  42262  ioodvbdlimc1lem1  42265  ioodvbdlimc1lem2  42266  ioodvbdlimc1  42267  ioodvbdlimc2lem  42268  ioodvbdlimc2  42269  dvnprodlem2  42281  voliooicof  42330  volicofmpt  42331  stoweidlem39  42373  stoweidlem59  42393  dirkercncflem3  42439  dirkercncf  42441  fourierdlem48  42488  fourierdlem49  42489  fourierdlem50  42490  fourierdlem51  42491  fourierdlem52  42492  fourierdlem54  42494  fourierdlem59  42499  fourierdlem70  42510  fourierdlem72  42512  fourierdlem73  42513  fourierdlem74  42514  fourierdlem75  42515  fourierdlem76  42516  fourierdlem79  42519  fourierdlem84  42524  fourierdlem85  42525  fourierdlem88  42528  fourierdlem93  42533  fourierdlem94  42534  fourierdlem96  42536  fourierdlem97  42537  fourierdlem98  42538  fourierdlem99  42539  fourierdlem102  42542  fourierdlem103  42543  fourierdlem104  42544  fourierdlem111  42551  fourierdlem112  42552  fourierdlem113  42553  fourierdlem114  42554  fouriercn  42566  elaa2lem  42567  rrxtopnfi  42621  rrndistlt  42624  ioorrnopnlem  42638  issalnnd  42677  fge0icoicc  42696  fge0iccre  42705  sge0isum  42758  sge0gtfsumgt  42774  sge0seq  42777  ismeannd  42798  meaiuninclem  42811  caragenunicl  42855  caratheodorylem1  42857  caratheodorylem2  42858  isomenndlem  42861  elhoi  42873  hoicvr  42879  sge0hsphoire  42920  hoidmv1le  42925  hoiqssbllem3  42955  hspmbllem2  42958  ovolval2lem  42974  ovolval3  42978  ovolval4lem2  42981  ovolval5lem2  42984  ovolval5lem3  42985  ovnovollem1  42987  ovnovollem2  42988  iunhoiioolem  43006  iccvonmbllem  43009  vonioolem2  43012  vonioo  43013  smfco  43126  nnsum3primesgbe  44006  nnsum4primesodd  44010  nnsum4primesoddALTV  44011  1hegrlfgr  44056  funcringcsetcALTV2lem8  44363  funcringcsetclem8ALTV  44386  mapsnop  44442  mapprop  44443  zlmodzxzel  44452  snlindsntorlem  44574  refdivmptf  44651  refdivmptfv  44655  elbigolo1  44666  prelrrx2  44749  line2  44788  line2x  44790  line2y  44791  amgmwlem  44952