Theorem fssd 6720

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3899  ⟶wf 6529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ss 3916  df-f 6537

This theorem is used by:  fconst6g  6764  f1ounsn  7273  fsnex  7284  tposf2  8248  mapsnd  8893  mapss  8896  ralxpmap  8903  ac6sfi  9254  infpwfien  10065  infmap2  10219  cofsmo  10271  fin23lem32  10346  axdc3lem4  10455  pwfseqlem4a  10670  fseq1p1m1  13653  seqf1olem2  14106  wrdlen2i  15013  supcvg  15945  vdwlem8  17080  isacs2  17741  funcres2b  17986  funcestrcsetclem8  18235  funcsetcestrclem8  18250  gsumress  18784  gsumwsubmcl  18946  gsumws1  18947  pj1ghm  19830  gsumval3eu  20031  gsumval3  20034  gsumsubmcl  20046  gsumzadd  20049  gsumzoppg  20071  dprdsn  20165  pwssplit1  21243  pjdm2  21924  evlsvvval  22309  psdmul  22394  mat1dimelbas  22693  cnrest2  23511  cnprest2  23515  1stcelcls  23687  xkoptsub  23880  tsmssubm  24369  cncfss  25127  ipcn  25474  equivcau  25528  lmcau  25541  rrx0el  25626  i1fmulclem  25930  i1fres  25933  mbfi1fseqlem4  25946  itg2mulclem  25974  limccnp  26118  dvcmulf  26172  dvcobr  26173  dvcnvlem  26203  dvcnv  26204  dvef  26207  elply2  26421  plyeq0lem  26436  plyaddlem  26441  plymullem  26442  dgrlem  26455  coeidlem  26463  jensenlem2  27224  jensen  27225  om2noseqlt  28564  om2noseqlt2  28565  om2noseqf1o  28566  umgrupgr  29560  upgr1e  29570  umgrislfupgr  29580  usgrislfuspgr  29647  upgrres1  29773  umgrres1  29774  umgr2v2e  29985  0clwlkv  30601  minvecolem3  31357  minvecolem4  31361  occllem  31784  chscllem2  32119  chscllem4  32121  pjhf  32189  elrgspnsubrunlem1  33687  gsumind  33785  islinds5  33802  ellspds  33803  linds2eq  33814  1arithidomlem2  33946  1arithidom  33947  dfufd2lem  33959  selvply1rhmlemb  34029  mplmulmvr  34049  psrmonprod  34062  mplgsum  34063  esplyfval0  34074  esplylem  34076  esplympl  34077  esplyfv1  34079  esplyfval3  34082  esplyfval1  34083  esplyfvaln  34084  esplyind  34085  fedgmullem1  34139  fedgmullem2  34140  locfinref  34351  esumsnf  34574  hashreprin  35128  poimirlem29  38398  dochpolN  42363  aks6d1c7lem1  43046  evlsbagval  43432  evlsmhpvvval  43441  mhphf  43443  ismrc  43546  mapfzcons  43561  pwssplit4  43930  ntrf2  44964  binomcxplemnn0  45173  fcomptss  46034  fcoss  46040  frexr  46214  climreeq  46443  limccog  46450  limcrecl  46459  limsupre  46469  liminflimsupclim  46635  cncficcgt0  46716  dvdivcncf  46755  dvbdfbdioolem1  46756  ioodvbdlimc1lem1  46759  ioodvbdlimc1lem2  46760  ioodvbdlimc1  46761  ioodvbdlimc2lem  46762  ioodvbdlimc2  46763  dvnprodlem2  46775  voliooicof  46824  volicofmpt  46825  stoweidlem39  46867  stoweidlem59  46887  dirkercncflem3  46933  dirkercncf  46935  fourierdlem48  46982  fourierdlem49  46983  fourierdlem50  46984  fourierdlem51  46985  fourierdlem52  46986  fourierdlem54  46988  fourierdlem59  46993  fourierdlem70  47004  fourierdlem72  47006  fourierdlem73  47007  fourierdlem74  47008  fourierdlem75  47009  fourierdlem76  47010  fourierdlem79  47013  fourierdlem84  47018  fourierdlem85  47019  fourierdlem88  47022  fourierdlem93  47027  fourierdlem94  47028  fourierdlem96  47030  fourierdlem97  47031  fourierdlem98  47032  fourierdlem99  47033  fourierdlem102  47036  fourierdlem103  47037  fourierdlem104  47038  fourierdlem111  47045  fourierdlem112  47046  fourierdlem113  47047  fourierdlem114  47048  fouriercn  47060  elaa2lem  47061  rrxtopnfi  47115  rrndistlt  47118  ioorrnopnlem  47132  issalnnd  47173  fge0icoicc  47193  fge0iccre  47202  sge0isum  47255  sge0gtfsumgt  47271  sge0seq  47274  ismeannd  47295  meaiuninclem  47308  caragenunicl  47352  caratheodorylem1  47354  caratheodorylem2  47355  isomenndlem  47358  elhoi  47370  sge0hsphoire  47417  hoidmv1le  47422  hoiqssbllem3  47452  hspmbllem2  47455  ovolval2lem  47471  ovolval3  47475  ovolval4lem2  47478  ovolval5lem2  47481  ovnovollem1  47484  ovnovollem2  47485  iunhoiioolem  47503  iccvonmbllem  47506  vonioolem2  47509  vonioo  47510  smfco  47630  nnsum3primesgbe  48708  nnsum4primesodd  48712  nnsum4primesoddALTV  48713  grimuhgr  48803  uhgrimisgrgric  48847  isubgr3stgrlem6  48887  1hegrlfgr  49048  funcringcsetcALTV2lem8  49212  funcringcsetclem8ALTV  49235  mapsnop  49274  fprmappr  49275  zlmodzxzel  49285  snlindsntorlem  49400  refdivmptf  49472  refdivmptfv  49476  elbigolo1  49487  2arymaptfo  49584  prelrrx2  49643  line2  49682  line2x  49684  line2y  49685  amgmwlem  50820