Theorem fvco3 6991

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 6718	. 2 ⊢ (𝐺:𝐴⟶𝐵 → 𝐺 Fn 𝐴)
2		fvco2 6989	. 2 ⊢ ((𝐺 Fn 𝐴 ∧ 𝐶 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶)))
3	1, 2	sylan 581	1 ⊢ ((𝐺:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶)))

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107   ∘ ccom 5681   Fn wfn 6539  ⟶wf 6540  ‘cfv 6544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552

This theorem is referenced by:  fvco3d  6992  foco2  7109  f1cofveqaeqALT  7258  f1ocnvfv1  7274  f1ocnvfv2  7275  fcof1  7285  fcofo  7286  cocan1  7289  cocan2  7290  fveqf1o  7301  isotr  7333  fipreima  9358  fsuppco2  9398  fsuppcor  9399  unxpwdom2  9583  wemapwe  9692  ackbij2lem2  10235  cofsmo  10264  cfcoflem  10267  isf32lem6  10353  isf32lem7  10354  isf32lem8  10355  isf34lem7  10374  isf34lem6  10375  axcc3  10433  axdc4lem  10450  inar1  10770  axdc4uzlem  13948  seqf1olem2  14008  seqf1o  14009  lswco  14790  lo1o1  15476  o1co  15530  caucvgrlem2  15621  summolem3  15660  fsumf1o  15669  fsumcl2lem  15677  fsumadd  15686  fsummulc2  15730  fsumrelem  15753  supcvg  15802  prodmolem3  15877  fprodf1o  15890  fprodser  15893  fprodcl2lem  15894  fprodmul  15904  fproddiv  15905  fprodn0  15923  ruclem11  16183  ruclem12  16184  algcvg  16513  eulerthlem2  16715  cofu1  17834  cofu2  17836  cofucl  17838  fucidcl  17918  fuclid  17919  fucrid  17920  homadm  17990  homacd  17991  evlfcl  18175  curfuncf  18191  yonedalem4c  18230  yonedalem3b  18232  mhmco  18704  prdspjmhm  18710  pwsco1mhm  18713  lactghmga  19273  frgpup3lem  19645  gsumval3eu  19772  gsumval3  19775  gsumzaddlem  19789  gsumzmhm  19805  dprdf1o  19902  gsumfsum  21012  zrhpsgninv  21138  zrhpsgnevpm  21144  zrhpsgnodpm  21145  evlssca  21652  evls1val  21839  evls1sca  21842  evl1val  21848  mdetralt  22110  mdetunilem7  22120  cpmadumatpoly  22385  chcoeffeqlem  22387  cnpco  22771  lmcnp  22808  upxp  23127  uptx  23129  cnmpt11  23167  cnmpt21  23175  xkofvcn  23188  prdstmdd  23628  prdstgpd  23629  comet  24022  prdsxmslem2  24038  nrmmetd  24083  isngp3  24107  ngpds  24113  tngnm  24168  nmoco  24254  cnmetdval  24287  climcncf  24416  cncfco  24423  htpyco1  24494  htpyco2  24495  phtpyco2  24506  reparphti  24513  copco  24534  pi1cof  24575  pi1coghm  24577  caubl  24825  caublcls  24826  cniccbdd  24978  ovolfioo  24984  ovolficc  24985  ovolfsval  24987  ovolicc2lem1  25034  ovolicc2lem4  25037  ovolicc2lem5  25038  volsup  25073  uniiccdif  25095  uniioovol  25096  uniiccvol  25097  uniioombllem2  25100  uniioombllem3a  25101  uniioombllem4  25103  uniioombllem5  25104  mbfimaopnlem  25172  limccnp  25408  dvcobr  25463  dvcjbr  25466  dvfre  25468  plycjlem  25790  plycj  25791  coecj  25792  radcnvlem2  25926  radcnvlem3  25927  radcnvlt2  25931  pserulm  25934  resinf1o  26045  jensen  26493  eflgam  26549  ftalem3  26579  dchrinv  26764  dchr2sum  26776  dchrisum0re  27016  motco  27791  motcgrg  27795  ex-co  29691  vafval  29856  smfval  29858  vsfval  29886  imsdval  29939  lnocoi  30010  occllem  30556  hocoi  31017  homco1  31054  counop  31174  homco2  31230  hmopco  31276  nlelchi  31314  kbass2  31370  kbass5  31373  leopsq  31382  hmopidmchi  31404  elpjrn  31443  pjinvari  31444  cycpmco2  32292  derangenlem  34162  subfacp1lem5  34175  cnpconn  34221  txsconnlem  34231  txsconn  34232  cvmliftmolem1  34272  cvmliftlem7  34282  cvmlift2lem3  34296  cvmlift2lem7  34300  cvmlift2lem9  34302  cvmliftphtlem  34308  cvmlift3lem1  34310  cvmlift3lem2  34311  cvmlift3lem4  34313  cvmlift3lem5  34314  cvmlift3lem6  34315  cvmlift3lem7  34316  mrsubco  34512  msubco  34522  mclsppslem  34574  sinccvglem  34657  iprodefisumlem  34710  iprodefisum  34711  gg-reparphti  35172  gg-dvcobr  35176  poimirlem22  36510  mblfinlem2  36526  ftc1anclem5  36565  ftc1anclem8  36568  cocanfo  36587  f1ocan1fv  36594  upixp  36597  ghomco  36759  rngohomco  36842  lautco  38968  ldilco  38987  ltrncoval  39016  tendocoval  39637  tendoconid  39700  tendospass  39890  dicvscacl  40062  cdlemn3  40068  cdlemn9  40076  brcoffn  42781  fvovco  43892  climexp  44321  stoweidlem27  44743  stoweidlem31  44747  ovolval4lem1  45365  isomushgr  46494  mgmhmco  46571