Theorem fvco3 6982

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149   ∘ ccom 5666   Fn wfn 6532  ⟶wf 6533  ‘cfv 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545

This theorem is referenced by:  fvco3d  6983  foco2  7105  f1cofveqaeqALT  7257  f1ocnvfv1  7275  f1ocnvfv2  7276  fcof1  7286  fcofo  7287  cocan1  7290  cocan2  7291  fveqf1o  7301  isotr  7335  fipreima  9314  fsuppco2  9362  fsuppcor  9363  unxpwdom2  9549  wemapwe  9665  ackbij2lem2  10221  cofsmo  10252  cfcoflem  10255  isf32lem6  10341  isf32lem7  10342  isf32lem8  10343  isf34lem7  10362  isf34lem6  10363  axcc3  10421  axdc4lem  10438  inar1  10759  axdc4uzlem  14018  seqf1olem2  14077  seqf1o  14078  lswco  14875  lo1o1  15582  o1co  15636  caucvgrlem2  15725  summolem3  15764  fsumf1o  15773  fsumcl2lem  15781  fsumadd  15790  fsummulc2  15834  fsumrelem  15858  supcvg  15909  prodmolem3  15986  fprodf1o  15999  fprodser  16002  fprodcl2lem  16003  fprodmul  16013  fproddiv  16014  fprodn0  16032  ruclem11  16295  ruclem12  16296  algcvg  16633  eulerthlem2  16840  cofu1  17940  cofu2  17942  cofucl  17944  fucidcl  18024  fuclid  18025  fucrid  18026  homadm  18096  homacd  18097  evlfcl  18277  curfuncf  18293  yonedalem4c  18332  yonedalem3b  18334  mgmhmco  18771  mhmco  18881  prdspjmhm  18887  pwsco1mhm  18890  lactghmga  19474  frgpup3lem  19846  gsumval3eu  19973  gsumval3  19976  gsumzaddlem  19990  gsumzmhm  20006  dprdf1o  20103  gsumfsum  21552  zrhpsgninv  21703  zrhpsgnevpm  21709  zrhpsgnodpm  21710  evlssca  22213  evls1val  22448  evls1sca  22451  evl1val  22457  mdetralt  22733  mdetunilem7  22743  cpmadumatpoly  23008  chcoeffeqlem  23010  cnpco  23392  lmcnp  23429  upxp  23748  uptx  23750  cnmpt11  23788  cnmpt21  23796  xkofvcn  23809  prdstmdd  24249  prdstgpd  24250  comet  24638  prdsxmslem2  24654  nrmmetd  24699  isngp3  24723  ngpds  24729  tngnm  24776  nmoco  24862  cnmetdval  24895  climcncf  25027  cncfco  25034  htpyco1  25105  htpyco2  25106  phtpyco2  25117  reparphti  25124  copco  25145  pi1cof  25186  pi1coghm  25188  caubl  25435  caublcls  25436  cniccbdd  25588  ovolfioo  25594  ovolficc  25595  ovolfsval  25597  ovolicc2lem1  25644  ovolicc2lem4  25647  ovolicc2lem5  25648  volsup  25683  uniiccdif  25705  uniioovol  25706  uniiccvol  25707  uniioombllem2  25710  uniioombllem3a  25711  uniioombllem4  25713  uniioombllem5  25714  mbfimaopnlem  25782  limccnp  26018  dvcobr  26073  dvcjbr  26076  dvfre  26078  plycjlem  26401  plycj  26402  coecj  26403  plycjOLD  26404  coecjOLD  26405  radcnvlem2  26542  radcnvlem3  26543  radcnvlt2  26547  pserulm  26550  resinf1o  26666  jensen  27118  eflgam  27174  ftalem3  27204  dchrinv  27390  dchr2sum  27402  dchrisum0re  27642  motco  28774  motcgrg  28778  ex-co  30729  vafval  30895  smfval  30897  vsfval  30925  imsdval  30978  lnocoi  31049  occllem  31595  hocoi  32056  homco1  32093  counop  32213  homco2  32269  hmopco  32315  nlelchi  32353  kbass2  32409  kbass5  32412  leopsq  32421  hmopidmchi  32443  elpjrn  32482  pjinvari  32483  cycpmco2  33393  derangenlem  35561  subfacp1lem5  35574  cnpconn  35620  txsconnlem  35630  txsconn  35631  cvmliftmolem1  35671  cvmliftlem7  35681  cvmlift2lem3  35695  cvmlift2lem7  35699  cvmlift2lem9  35701  cvmliftphtlem  35707  cvmlift3lem1  35709  cvmlift3lem2  35710  cvmlift3lem4  35712  cvmlift3lem5  35713  cvmlift3lem6  35714  cvmlift3lem7  35715  mrsubco  35911  msubco  35921  mclsppslem  35973  sinccvglem  36062  iprodefisumlem  36130  iprodefisum  36131  poimirlem22  38180  mblfinlem2  38196  ftc1anclem5  38235  ftc1anclem8  38238  cocanfo  38257  f1ocan1fv  38264  upixp  38267  ghomco  38429  rngohomco  38512  lautco  40760  ldilco  40779  ltrncoval  40808  tendocoval  41429  tendoconid  41492  tendospass  41682  dicvscacl  41854  cdlemn3  41860  cdlemn9  41868  brcoffn  44647  fvovco  45802  climexp  46212  stoweidlem27  46632  stoweidlem31  46636  ovolval4lem1  47254  gricushgr  48570  uspgrlimlem3  48643  uspgrlimlem4  48644  grlictr  48668