Theorem fssd 6708

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

Syntax hints:   → wi 4   ⊆ wss 3917  ⟶wf 6510

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 3934  df-f 6518

This theorem is referenced by:  fconst6g  6752  f1ounsn  7250  fsnex  7261  tposf2  8232  mapsnd  8862  mapss  8865  ralxpmap  8872  ac6sfi  9238  infpwfien  10022  infmap2  10177  cofsmo  10229  fin23lem32  10304  axdc3lem4  10413  pwfseqlem4a  10621  fseq1p1m1  13566  seqf1olem2  14014  wrdlen2i  14915  supcvg  15829  vdwlem8  16966  isacs2  17621  funcres2b  17866  funcestrcsetclem8  18115  funcsetcestrclem8  18130  gsumress  18616  gsumwsubmcl  18771  gsumws1  18772  pj1ghm  19640  gsumval3eu  19841  gsumval3  19844  gsumsubmcl  19856  gsumzadd  19859  gsumzoppg  19881  dprdsn  19975  pwssplit1  20973  pjdm2  21627  psdmul  22060  mat1dimelbas  22365  cnrest2  23180  cnprest2  23184  1stcelcls  23355  xkoptsub  23548  tsmssubm  24037  cncfss  24799  ipcn  25153  equivcau  25207  lmcau  25220  rrx0el  25305  i1fmulclem  25610  i1fres  25613  mbfi1fseqlem4  25626  itg2mulclem  25654  limccnp  25799  dvcmulf  25855  dvcobr  25856  dvcobrOLD  25857  dvcnvlem  25887  dvcnv  25888  dvef  25891  elply2  26108  plyeq0lem  26122  plyaddlem  26127  plymullem  26128  dgrlem  26141  coeidlem  26149  jensenlem2  26905  jensen  26906  om2noseqlt  28200  om2noseqlt2  28201  om2noseqf1o  28202  umgrupgr  29037  upgr1e  29047  umgrislfupgr  29057  usgrislfuspgr  29121  upgrres1  29247  umgrres1  29248  umgr2v2e  29460  0clwlkv  30067  minvecolem3  30812  minvecolem4  30816  occllem  31239  chscllem2  31574  chscllem4  31576  pjhf  31644  elrgspnsubrunlem1  33205  islinds5  33345  ellspds  33346  linds2eq  33359  1arithidomlem2  33514  1arithidom  33515  dfufd2lem  33527  fedgmullem1  33632  fedgmullem2  33633  locfinref  33838  esumsnf  34061  hashreprin  34618  poimirlem29  37650  dochpolN  41491  aks6d1c7lem1  42175  evlsvvval  42558  evlsbagval  42561  evlsmhpvvval  42590  mhphf  42592  ismrc  42696  mapfzcons  42711  pwssplit4  43085  ntrf2  44120  binomcxplemnn0  44345  fcomptss  45204  fcoss  45211  frexr  45388  climreeq  45618  limccog  45625  limcrecl  45634  limsupre  45646  liminflimsupclim  45812  cncficcgt0  45893  dvdivcncf  45932  dvbdfbdioolem1  45933  ioodvbdlimc1lem1  45936  ioodvbdlimc1lem2  45937  ioodvbdlimc1  45938  ioodvbdlimc2lem  45939  ioodvbdlimc2  45940  dvnprodlem2  45952  voliooicof  46001  volicofmpt  46002  stoweidlem39  46044  stoweidlem59  46064  dirkercncflem3  46110  dirkercncf  46112  fourierdlem48  46159  fourierdlem49  46160  fourierdlem50  46161  fourierdlem51  46162  fourierdlem52  46163  fourierdlem54  46165  fourierdlem59  46170  fourierdlem70  46181  fourierdlem72  46183  fourierdlem73  46184  fourierdlem74  46185  fourierdlem75  46186  fourierdlem76  46187  fourierdlem79  46190  fourierdlem84  46195  fourierdlem85  46196  fourierdlem88  46199  fourierdlem93  46204  fourierdlem94  46205  fourierdlem96  46207  fourierdlem97  46208  fourierdlem98  46209  fourierdlem99  46210  fourierdlem102  46213  fourierdlem103  46214  fourierdlem104  46215  fourierdlem111  46222  fourierdlem112  46223  fourierdlem113  46224  fourierdlem114  46225  fouriercn  46237  elaa2lem  46238  rrxtopnfi  46292  rrndistlt  46295  ioorrnopnlem  46309  issalnnd  46350  fge0icoicc  46370  fge0iccre  46379  sge0isum  46432  sge0gtfsumgt  46448  sge0seq  46451  ismeannd  46472  meaiuninclem  46485  caragenunicl  46529  caratheodorylem1  46531  caratheodorylem2  46532  isomenndlem  46535  elhoi  46547  hoicvr  46553  sge0hsphoire  46594  hoidmv1le  46599  hoiqssbllem3  46629  hspmbllem2  46632  ovolval2lem  46648  ovolval3  46652  ovolval4lem2  46655  ovolval5lem2  46658  ovnovollem1  46661  ovnovollem2  46662  iunhoiioolem  46680  iccvonmbllem  46683  vonioolem2  46686  vonioo  46687  smfco  46807  nnsum3primesgbe  47797  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  grimuhgr  47891  uhgrimisgrgric  47935  isubgr3stgrlem6  47974  1hegrlfgr  48124  funcringcsetcALTV2lem8  48289  funcringcsetclem8ALTV  48312  mapsnop  48336  fprmappr  48337  zlmodzxzel  48347  snlindsntorlem  48463  refdivmptf  48535  refdivmptfv  48539  elbigolo1  48550  2arymaptfo  48647  prelrrx2  48706  line2  48745  line2x  48747  line2y  48748  amgmwlem  49795