Theorem fvco3 6987

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106   ∘ ccom 5679   Fn wfn 6535  ⟶wf 6536  ‘cfv 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548

This theorem is referenced by:  fvco3d  6988  foco2  7105  f1cofveqaeqALT  7254  f1ocnvfv1  7270  f1ocnvfv2  7271  fcof1  7281  fcofo  7282  cocan1  7285  cocan2  7286  fveqf1o  7297  isotr  7329  fipreima  9354  fsuppco2  9394  fsuppcor  9395  unxpwdom2  9579  wemapwe  9688  ackbij2lem2  10231  cofsmo  10260  cfcoflem  10263  isf32lem6  10349  isf32lem7  10350  isf32lem8  10351  isf34lem7  10370  isf34lem6  10371  axcc3  10429  axdc4lem  10446  inar1  10766  axdc4uzlem  13944  seqf1olem2  14004  seqf1o  14005  lswco  14786  lo1o1  15472  o1co  15526  caucvgrlem2  15617  summolem3  15656  fsumf1o  15665  fsumcl2lem  15673  fsumadd  15682  fsummulc2  15726  fsumrelem  15749  supcvg  15798  prodmolem3  15873  fprodf1o  15886  fprodser  15889  fprodcl2lem  15890  fprodmul  15900  fproddiv  15901  fprodn0  15919  ruclem11  16179  ruclem12  16180  algcvg  16509  eulerthlem2  16711  cofu1  17830  cofu2  17832  cofucl  17834  fucidcl  17914  fuclid  17915  fucrid  17916  homadm  17986  homacd  17987  evlfcl  18171  curfuncf  18187  yonedalem4c  18226  yonedalem3b  18228  mhmco  18700  prdspjmhm  18706  pwsco1mhm  18709  lactghmga  19267  frgpup3lem  19639  gsumval3eu  19766  gsumval3  19769  gsumzaddlem  19783  gsumzmhm  19799  dprdf1o  19896  gsumfsum  21004  zrhpsgninv  21129  zrhpsgnevpm  21135  zrhpsgnodpm  21136  evlssca  21643  evls1val  21830  evls1sca  21833  evl1val  21839  mdetralt  22101  mdetunilem7  22111  cpmadumatpoly  22376  chcoeffeqlem  22378  cnpco  22762  lmcnp  22799  upxp  23118  uptx  23120  cnmpt11  23158  cnmpt21  23166  xkofvcn  23179  prdstmdd  23619  prdstgpd  23620  comet  24013  prdsxmslem2  24029  nrmmetd  24074  isngp3  24098  ngpds  24104  tngnm  24159  nmoco  24245  cnmetdval  24278  climcncf  24407  cncfco  24414  htpyco1  24485  htpyco2  24486  phtpyco2  24497  reparphti  24504  copco  24525  pi1cof  24566  pi1coghm  24568  caubl  24816  caublcls  24817  cniccbdd  24969  ovolfioo  24975  ovolficc  24976  ovolfsval  24978  ovolicc2lem1  25025  ovolicc2lem4  25028  ovolicc2lem5  25029  volsup  25064  uniiccdif  25086  uniioovol  25087  uniiccvol  25088  uniioombllem2  25091  uniioombllem3a  25092  uniioombllem4  25094  uniioombllem5  25095  mbfimaopnlem  25163  limccnp  25399  dvcobr  25454  dvcjbr  25457  dvfre  25459  plycjlem  25781  plycj  25782  coecj  25783  radcnvlem2  25917  radcnvlem3  25918  radcnvlt2  25922  pserulm  25925  resinf1o  26036  jensen  26482  eflgam  26538  ftalem3  26568  dchrinv  26753  dchr2sum  26765  dchrisum0re  27005  motco  27780  motcgrg  27784  ex-co  29680  vafval  29843  smfval  29845  vsfval  29873  imsdval  29926  lnocoi  29997  occllem  30543  hocoi  31004  homco1  31041  counop  31161  homco2  31217  hmopco  31263  nlelchi  31301  kbass2  31357  kbass5  31360  leopsq  31369  hmopidmchi  31391  elpjrn  31430  pjinvari  31431  cycpmco2  32279  derangenlem  34150  subfacp1lem5  34163  cnpconn  34209  txsconnlem  34219  txsconn  34220  cvmliftmolem1  34260  cvmliftlem7  34270  cvmlift2lem3  34284  cvmlift2lem7  34288  cvmlift2lem9  34290  cvmliftphtlem  34296  cvmlift3lem1  34298  cvmlift3lem2  34299  cvmlift3lem4  34301  cvmlift3lem5  34302  cvmlift3lem6  34303  cvmlift3lem7  34304  mrsubco  34500  msubco  34510  mclsppslem  34562  sinccvglem  34645  iprodefisumlem  34698  iprodefisum  34699  gg-reparphti  35160  gg-dvcobr  35164  poimirlem22  36498  mblfinlem2  36514  ftc1anclem5  36553  ftc1anclem8  36556  cocanfo  36575  f1ocan1fv  36582  upixp  36585  ghomco  36747  rngohomco  36830  lautco  38956  ldilco  38975  ltrncoval  39004  tendocoval  39625  tendoconid  39688  tendospass  39878  dicvscacl  40050  cdlemn3  40056  cdlemn9  40064  brcoffn  42766  fvovco  43877  climexp  44307  stoweidlem27  44729  stoweidlem31  44733  ovolval4lem1  45351  isomushgr  46480  mgmhmco  46557