Theorem fssd 6727

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3906  ⟶wf 6536

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 3923  df-f 6544

This theorem is used by:  fconst6g  6771  f1ounsn  7279  fsnex  7290  tposf2  8252  mapsnd  8890  mapss  8893  ralxpmap  8900  ac6sfi  9251  infpwfien  10062  infmap2  10216  cofsmo  10268  fin23lem32  10343  axdc3lem4  10452  pwfseqlem4a  10661  fseq1p1m1  13643  seqf1olem2  14096  wrdlen2i  15003  supcvg  15933  vdwlem8  17070  isacs2  17731  funcres2b  17976  funcestrcsetclem8  18225  funcsetcestrclem8  18240  gsumress  18772  gsumwsubmcl  18933  gsumws1  18934  pj1ghm  19817  gsumval3eu  20018  gsumval3  20021  gsumsubmcl  20033  gsumzadd  20036  gsumzoppg  20058  dprdsn  20152  pwssplit1  21230  pjdm2  21911  evlsvvval  22294  psdmul  22379  mat1dimelbas  22678  cnrest2  23493  cnprest2  23497  1stcelcls  23669  xkoptsub  23862  tsmssubm  24351  cncfss  25109  ipcn  25456  equivcau  25510  lmcau  25523  rrx0el  25608  i1fmulclem  25912  i1fres  25915  mbfi1fseqlem4  25928  itg2mulclem  25956  limccnp  26101  dvcmulf  26155  dvcobr  26156  dvcnvlem  26186  dvcnv  26187  dvef  26190  elply2  26404  plyeq0lem  26418  plyaddlem  26423  plymullem  26424  dgrlem  26437  coeidlem  26445  jensenlem2  27203  jensen  27204  om2noseqlt  28543  om2noseqlt2  28544  om2noseqf1o  28545  umgrupgr  29508  upgr1e  29518  umgrislfupgr  29528  usgrislfuspgr  29595  upgrres1  29721  umgrres1  29722  umgr2v2e  29933  0clwlkv  30549  minvecolem3  31299  minvecolem4  31303  occllem  31726  chscllem2  32061  chscllem4  32063  pjhf  32131  elrgspnsubrunlem1  33631  gsumind  33729  islinds5  33746  ellspds  33747  linds2eq  33758  1arithidomlem2  33890  1arithidom  33891  dfufd2lem  33903  selvply1rhmlemb  33973  mplmulmvr  33993  psrmonprod  34006  mplgsum  34007  esplyfval0  34018  esplylem  34020  esplympl  34021  esplyfv1  34023  esplyfval3  34026  esplyfval1  34027  esplyfvaln  34028  esplyind  34029  fedgmullem1  34083  fedgmullem2  34084  locfinref  34295  esumsnf  34518  hashreprin  35072  poimirlem29  38357  dochpolN  42322  aks6d1c7lem1  43005  evlsbagval  43376  evlsmhpvvval  43385  mhphf  43387  ismrc  43490  mapfzcons  43505  pwssplit4  43874  ntrf2  44908  binomcxplemnn0  45117  fcomptss  45978  fcoss  45984  frexr  46158  climreeq  46387  limccog  46394  limcrecl  46403  limsupre  46413  liminflimsupclim  46579  cncficcgt0  46660  dvdivcncf  46699  dvbdfbdioolem1  46700  ioodvbdlimc1lem1  46703  ioodvbdlimc1lem2  46704  ioodvbdlimc1  46705  ioodvbdlimc2lem  46706  ioodvbdlimc2  46707  dvnprodlem2  46719  voliooicof  46768  volicofmpt  46769  stoweidlem39  46811  stoweidlem59  46831  dirkercncflem3  46877  dirkercncf  46879  fourierdlem48  46926  fourierdlem49  46927  fourierdlem50  46928  fourierdlem51  46929  fourierdlem52  46930  fourierdlem54  46932  fourierdlem59  46937  fourierdlem70  46948  fourierdlem72  46950  fourierdlem73  46951  fourierdlem74  46952  fourierdlem75  46953  fourierdlem76  46954  fourierdlem79  46957  fourierdlem84  46962  fourierdlem85  46963  fourierdlem88  46966  fourierdlem93  46971  fourierdlem94  46972  fourierdlem96  46974  fourierdlem97  46975  fourierdlem98  46976  fourierdlem99  46977  fourierdlem102  46980  fourierdlem103  46981  fourierdlem104  46982  fourierdlem111  46989  fourierdlem112  46990  fourierdlem113  46991  fourierdlem114  46992  fouriercn  47004  elaa2lem  47005  rrxtopnfi  47059  rrndistlt  47062  ioorrnopnlem  47076  issalnnd  47117  fge0icoicc  47137  fge0iccre  47146  sge0isum  47199  sge0gtfsumgt  47215  sge0seq  47218  ismeannd  47239  meaiuninclem  47252  caragenunicl  47296  caratheodorylem1  47298  caratheodorylem2  47299  isomenndlem  47302  elhoi  47314  sge0hsphoire  47361  hoidmv1le  47366  hoiqssbllem3  47396  hspmbllem2  47399  ovolval2lem  47415  ovolval3  47419  ovolval4lem2  47422  ovolval5lem2  47425  ovnovollem1  47428  ovnovollem2  47429  iunhoiioolem  47447  iccvonmbllem  47450  vonioolem2  47453  vonioo  47454  smfco  47574  nnsum3primesgbe  48615  nnsum4primesodd  48619  nnsum4primesoddALTV  48620  grimuhgr  48710  uhgrimisgrgric  48754  isubgr3stgrlem6  48794  1hegrlfgr  48955  funcringcsetcALTV2lem8  49119  funcringcsetclem8ALTV  49142  mapsnop  49181  fprmappr  49182  zlmodzxzel  49192  snlindsntorlem  49307  refdivmptf  49379  refdivmptfv  49383  elbigolo1  49394  2arymaptfo  49491  prelrrx2  49550  line2  49589  line2x  49591  line2y  49592  amgmwlem  50707