Theorem fssd 6057

Description: Expanding the codomain of a mapping, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
fssd.f	|- ( ph -> F : A --> B )
fssd.b	|- ( ph -> B C_ C )

Assertion

Ref	Expression
fssd	|- ( ph -> F : A --> C )

Proof of Theorem fssd

Step	Hyp	Ref	Expression
1		fssd.f	. 2 |- ( ph -> F : A --> B )
2		fssd.b	. 2 |- ( ph -> B C_ C )
3		fss 6056	. 2 |- ( ( F : A --> B /\ B C_ C ) -> F : A --> C )
4	1, 2, 3	syl2anc 693	1 |- ( ph -> F : A --> C )

Syntax hints:   -> wi 4   C_ wss 3574   -->wf 5884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588  df-f 5892

This theorem is referenced by:  fconst6g  6094  tposf2  7376  mapss  7900  ralxpmap  7907  ac6sfi  8204  infpwfien  8885  infmap2  9040  cofsmo  9091  fin23lem32  9166  axdc3lem4  9275  pwfseqlem4a  9483  fseq1p1m1  12414  seqf1olem2  12841  wrdlen2i  13686  supcvg  14588  vdwlem8  15692  isacs2  16314  funcres2b  16557  funcestrcsetclem8  16787  funcsetcestrclem8  16802  gsumress  17276  gsumwsubmcl  17375  gsumws1  17376  pj1ghm  18116  gsumval3eu  18305  gsumval3  18308  gsumsubmcl  18319  gsumzadd  18322  gsumzoppg  18344  dprdsn  18435  pwssplit1  19059  pjdm2  20055  mat1dimelbas  20277  cnrest2  21090  cnprest2  21094  1stcelcls  21264  xkoptsub  21457  tsmssubm  21946  cncfss  22702  ipcn  23045  equivcau  23098  lmcau  23111  i1fmulclem  23469  i1fres  23472  mbfi1fseqlem4  23485  itg2mulclem  23513  limccnp  23655  dvcmulf  23708  dvcobr  23709  dvcnvlem  23739  dvcnv  23740  dvef  23743  elply2  23952  plyeq0lem  23966  plyaddlem  23971  plymullem  23972  dgrlem  23985  coeidlem  23993  jensenlem2  24714  jensen  24715  umgrupgr  25998  upgr1e  26008  umgrislfupgr  26018  usgrislfuspgr  26079  upgrres1  26205  umgrres1  26206  umgr2v2e  26421  minvecolem3  27732  minvecolem4  27736  occllem  28162  chscllem2  28497  chscllem4  28499  pjhf  28567  locfinref  29908  esumsnf  30126  hashreprin  30698  poimirlem29  33438  dochpolN  36779  ismrc  37264  mapfzcons  37279  pwssplit4  37659  ntrf2  38422  binomcxplemnn0  38548  fcomptss  39395  fcoss  39402  fco3  39421  frexr  39604  climreeq  39845  limccog  39852  limcrecl  39861  limsupre  39873  liminflimsupclim  40039  cncficcgt0  40101  dvdivcncf  40142  dvbdfbdioolem1  40143  ioodvbdlimc1lem1  40146  ioodvbdlimc1lem2  40147  ioodvbdlimc1  40148  ioodvbdlimc2lem  40149  ioodvbdlimc2  40150  dvnprodlem2  40162  voliooicof  40213  volicofmpt  40214  stoweidlem39  40256  stoweidlem59  40276  dirkercncflem3  40322  dirkercncf  40324  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem51  40374  fourierdlem52  40375  fourierdlem54  40377  fourierdlem59  40382  fourierdlem70  40393  fourierdlem72  40395  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem79  40402  fourierdlem84  40407  fourierdlem85  40408  fourierdlem88  40411  fourierdlem93  40416  fourierdlem94  40417  fourierdlem96  40419  fourierdlem97  40420  fourierdlem98  40421  fourierdlem99  40422  fourierdlem102  40425  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  fourierdlem112  40435  fourierdlem113  40436  fourierdlem114  40437  fouriercn  40449  elaa2lem  40450  rrxtopnfi  40506  rrndistlt  40510  ioorrnopnlem  40524  issalnnd  40563  fge0icoicc  40582  fge0iccre  40591  sge0isum  40644  sge0gtfsumgt  40660  sge0seq  40663  ismeannd  40684  meaiuninclem  40697  caragenunicl  40738  caratheodorylem1  40740  caratheodorylem2  40741  isomenndlem  40744  elhoi  40756  hoicvr  40762  sge0hsphoire  40803  hoidmv1le  40808  hoiqssbllem3  40838  hspmbllem2  40841  ovolval2lem  40857  ovolval3  40861  ovolval4lem2  40864  ovolval5lem2  40867  ovolval5lem3  40868  ovnovollem1  40870  ovnovollem2  40871  iunhoiioolem  40889  iccvonmbllem  40892  vonioolem2  40895  vonioo  40896  smfco  41009  nnsum3primesgbe  41680  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  1hegrlfgr  41713  funcringcsetcALTV2lem8  42043  funcringcsetclem8ALTV  42066  mapsnop  42123  mapprop  42124  zlmodzxzel  42133  snlindsntorlem  42259  refdivmptf  42336  refdivmptfv  42340  elbigolo1  42351  amgmwlem  42548