Theorem fvco3 6933

Description: Value of a function composition. (Contributed by NM, 3-Jan-2004.) (Revised by Mario Carneiro, 26-Dec-2014.)

Assertion

Ref	Expression
fvco3	⊢ ((𝐺:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶)))

Proof of Theorem fvco3

Step	Hyp	Ref	Expression
1		ffn 6662	. 2 ⊢ (𝐺:𝐴⟶𝐵 → 𝐺 Fn 𝐴)
2		fvco2 6931	. 2 ⊢ ((𝐺 Fn 𝐴 ∧ 𝐶 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶)))
3	1, 2	sylan 580	1 ⊢ ((𝐺:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶)))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ∘ ccom 5628   Fn wfn 6487  ⟶wf 6488  ‘cfv 6492

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500

This theorem is referenced by:  fvco3d  6934  foco2  7054  f1cofveqaeqALT  7204  f1ocnvfv1  7222  f1ocnvfv2  7223  fcof1  7233  fcofo  7234  cocan1  7237  cocan2  7238  fveqf1o  7248  isotr  7282  fipreima  9258  fsuppco2  9306  fsuppcor  9307  unxpwdom2  9493  wemapwe  9606  ackbij2lem2  10149  cofsmo  10179  cfcoflem  10182  isf32lem6  10268  isf32lem7  10269  isf32lem8  10270  isf34lem7  10289  isf34lem6  10290  axcc3  10348  axdc4lem  10365  inar1  10686  axdc4uzlem  13906  seqf1olem2  13965  seqf1o  13966  lswco  14762  lo1o1  15455  o1co  15509  caucvgrlem2  15598  summolem3  15637  fsumf1o  15646  fsumcl2lem  15654  fsumadd  15663  fsummulc2  15707  fsumrelem  15730  supcvg  15779  prodmolem3  15856  fprodf1o  15869  fprodser  15872  fprodcl2lem  15873  fprodmul  15883  fproddiv  15884  fprodn0  15902  ruclem11  16165  ruclem12  16166  algcvg  16503  eulerthlem2  16709  cofu1  17808  cofu2  17810  cofucl  17812  fucidcl  17892  fuclid  17893  fucrid  17894  homadm  17964  homacd  17965  evlfcl  18145  curfuncf  18161  yonedalem4c  18200  yonedalem3b  18202  mgmhmco  18639  mhmco  18748  prdspjmhm  18754  pwsco1mhm  18757  lactghmga  19334  frgpup3lem  19706  gsumval3eu  19833  gsumval3  19836  gsumzaddlem  19850  gsumzmhm  19866  dprdf1o  19963  gsumfsum  21389  zrhpsgninv  21540  zrhpsgnevpm  21546  zrhpsgnodpm  21547  evlssca  22049  evls1val  22264  evls1sca  22267  evl1val  22273  mdetralt  22552  mdetunilem7  22562  cpmadumatpoly  22827  chcoeffeqlem  22829  cnpco  23211  lmcnp  23248  upxp  23567  uptx  23569  cnmpt11  23607  cnmpt21  23615  xkofvcn  23628  prdstmdd  24068  prdstgpd  24069  comet  24457  prdsxmslem2  24473  nrmmetd  24518  isngp3  24542  ngpds  24548  tngnm  24595  nmoco  24681  cnmetdval  24714  climcncf  24849  cncfco  24856  htpyco1  24933  htpyco2  24934  phtpyco2  24945  reparphti  24952  reparphtiOLD  24953  copco  24974  pi1cof  25015  pi1coghm  25017  caubl  25264  caublcls  25265  cniccbdd  25418  ovolfioo  25424  ovolficc  25425  ovolfsval  25427  ovolicc2lem1  25474  ovolicc2lem4  25477  ovolicc2lem5  25478  volsup  25513  uniiccdif  25535  uniioovol  25536  uniiccvol  25537  uniioombllem2  25540  uniioombllem3a  25541  uniioombllem4  25543  uniioombllem5  25544  mbfimaopnlem  25612  limccnp  25848  dvcobr  25905  dvcobrOLD  25906  dvcjbr  25909  dvfre  25911  plycjlem  26238  plycj  26239  coecj  26240  plycjOLD  26241  coecjOLD  26242  radcnvlem2  26379  radcnvlem3  26380  radcnvlt2  26384  pserulm  26387  resinf1o  26501  jensen  26955  eflgam  27011  ftalem3  27041  dchrinv  27228  dchr2sum  27240  dchrisum0re  27480  motco  28612  motcgrg  28616  ex-co  30513  vafval  30678  smfval  30680  vsfval  30708  imsdval  30761  lnocoi  30832  occllem  31378  hocoi  31839  homco1  31876  counop  31996  homco2  32052  hmopco  32098  nlelchi  32136  kbass2  32192  kbass5  32195  leopsq  32204  hmopidmchi  32226  elpjrn  32265  pjinvari  32266  cycpmco2  33215  derangenlem  35365  subfacp1lem5  35378  cnpconn  35424  txsconnlem  35434  txsconn  35435  cvmliftmolem1  35475  cvmliftlem7  35485  cvmlift2lem3  35499  cvmlift2lem7  35503  cvmlift2lem9  35505  cvmliftphtlem  35511  cvmlift3lem1  35513  cvmlift3lem2  35514  cvmlift3lem4  35516  cvmlift3lem5  35517  cvmlift3lem6  35518  cvmlift3lem7  35519  mrsubco  35715  msubco  35725  mclsppslem  35777  sinccvglem  35866  iprodefisumlem  35934  iprodefisum  35935  poimirlem22  37843  mblfinlem2  37859  ftc1anclem5  37898  ftc1anclem8  37901  cocanfo  37920  f1ocan1fv  37927  upixp  37930  ghomco  38092  rngohomco  38175  lautco  40357  ldilco  40376  ltrncoval  40405  tendocoval  41026  tendoconid  41089  tendospass  41279  dicvscacl  41451  cdlemn3  41457  cdlemn9  41465  brcoffn  44271  fvovco  45437  climexp  45851  stoweidlem27  46271  stoweidlem31  46275  ovolval4lem1  46893  gricushgr  48163  uspgrlimlem3  48236  uspgrlimlem4  48237  grlictr  48261