Theorem fvco3 7007

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105   ∘ ccom 5692   Fn wfn 6557  ⟶wf 6558  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fv 6570

This theorem is referenced by:  fvco3d  7008  foco2  7128  f1cofveqaeqALT  7278  f1ocnvfv1  7295  f1ocnvfv2  7296  fcof1  7306  fcofo  7307  cocan1  7310  cocan2  7311  fveqf1o  7321  isotr  7355  fipreima  9395  fsuppco2  9440  fsuppcor  9441  unxpwdom2  9625  wemapwe  9734  ackbij2lem2  10276  cofsmo  10306  cfcoflem  10309  isf32lem6  10395  isf32lem7  10396  isf32lem8  10397  isf34lem7  10416  isf34lem6  10417  axcc3  10475  axdc4lem  10492  inar1  10812  axdc4uzlem  14020  seqf1olem2  14079  seqf1o  14080  lswco  14874  lo1o1  15564  o1co  15618  caucvgrlem2  15707  summolem3  15746  fsumf1o  15755  fsumcl2lem  15763  fsumadd  15772  fsummulc2  15816  fsumrelem  15839  supcvg  15888  prodmolem3  15965  fprodf1o  15978  fprodser  15981  fprodcl2lem  15982  fprodmul  15992  fproddiv  15993  fprodn0  16011  ruclem11  16272  ruclem12  16273  algcvg  16609  eulerthlem2  16815  cofu1  17934  cofu2  17936  cofucl  17938  fucidcl  18021  fuclid  18022  fucrid  18023  homadm  18093  homacd  18094  evlfcl  18278  curfuncf  18294  yonedalem4c  18333  yonedalem3b  18335  mgmhmco  18739  mhmco  18848  prdspjmhm  18854  pwsco1mhm  18857  lactghmga  19437  frgpup3lem  19809  gsumval3eu  19936  gsumval3  19939  gsumzaddlem  19953  gsumzmhm  19969  dprdf1o  20066  gsumfsum  21469  zrhpsgninv  21620  zrhpsgnevpm  21626  zrhpsgnodpm  21627  evlssca  22130  evls1val  22339  evls1sca  22342  evl1val  22348  mdetralt  22629  mdetunilem7  22639  cpmadumatpoly  22904  chcoeffeqlem  22906  cnpco  23290  lmcnp  23327  upxp  23646  uptx  23648  cnmpt11  23686  cnmpt21  23694  xkofvcn  23707  prdstmdd  24147  prdstgpd  24148  comet  24541  prdsxmslem2  24557  nrmmetd  24602  isngp3  24626  ngpds  24632  tngnm  24687  nmoco  24773  cnmetdval  24806  climcncf  24939  cncfco  24946  htpyco1  25023  htpyco2  25024  phtpyco2  25035  reparphti  25042  reparphtiOLD  25043  copco  25064  pi1cof  25105  pi1coghm  25107  caubl  25355  caublcls  25356  cniccbdd  25509  ovolfioo  25515  ovolficc  25516  ovolfsval  25518  ovolicc2lem1  25565  ovolicc2lem4  25568  ovolicc2lem5  25569  volsup  25604  uniiccdif  25626  uniioovol  25627  uniiccvol  25628  uniioombllem2  25631  uniioombllem3a  25632  uniioombllem4  25634  uniioombllem5  25635  mbfimaopnlem  25703  limccnp  25940  dvcobr  25997  dvcobrOLD  25998  dvcjbr  26001  dvfre  26003  plycjlem  26330  plycj  26331  coecj  26332  plycjOLD  26333  coecjOLD  26334  radcnvlem2  26471  radcnvlem3  26472  radcnvlt2  26476  pserulm  26479  resinf1o  26592  jensen  27046  eflgam  27102  ftalem3  27132  dchrinv  27319  dchr2sum  27331  dchrisum0re  27571  motco  28562  motcgrg  28566  ex-co  30466  vafval  30631  smfval  30633  vsfval  30661  imsdval  30714  lnocoi  30785  occllem  31331  hocoi  31792  homco1  31829  counop  31949  homco2  32005  hmopco  32051  nlelchi  32089  kbass2  32145  kbass5  32148  leopsq  32157  hmopidmchi  32179  elpjrn  32218  pjinvari  32219  cycpmco2  33135  derangenlem  35155  subfacp1lem5  35168  cnpconn  35214  txsconnlem  35224  txsconn  35225  cvmliftmolem1  35265  cvmliftlem7  35275  cvmlift2lem3  35289  cvmlift2lem7  35293  cvmlift2lem9  35295  cvmliftphtlem  35301  cvmlift3lem1  35303  cvmlift3lem2  35304  cvmlift3lem4  35306  cvmlift3lem5  35307  cvmlift3lem6  35308  cvmlift3lem7  35309  mrsubco  35505  msubco  35515  mclsppslem  35567  sinccvglem  35656  iprodefisumlem  35719  iprodefisum  35720  poimirlem22  37628  mblfinlem2  37644  ftc1anclem5  37683  ftc1anclem8  37686  cocanfo  37705  f1ocan1fv  37712  upixp  37715  ghomco  37877  rngohomco  37960  lautco  40079  ldilco  40098  ltrncoval  40127  tendocoval  40748  tendoconid  40811  tendospass  41001  dicvscacl  41173  cdlemn3  41179  cdlemn9  41187  brcoffn  44019  fvovco  45135  climexp  45560  stoweidlem27  45982  stoweidlem31  45986  ovolval4lem1  46604  gricushgr  47823  uspgrlimlem3  47892  uspgrlimlem4  47893  grlictr  47910