Theorem fvco3 6922

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ∘ ccom 5623   Fn wfn 6477  ⟶wf 6478  ‘cfv 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-fv 6490

This theorem is referenced by:  fvco3d  6923  foco2  7043  f1cofveqaeqALT  7195  f1ocnvfv1  7213  f1ocnvfv2  7214  fcof1  7224  fcofo  7225  cocan1  7228  cocan2  7229  fveqf1o  7239  isotr  7273  fipreima  9248  fsuppco2  9293  fsuppcor  9294  unxpwdom2  9480  wemapwe  9593  ackbij2lem2  10133  cofsmo  10163  cfcoflem  10166  isf32lem6  10252  isf32lem7  10253  isf32lem8  10254  isf34lem7  10273  isf34lem6  10274  axcc3  10332  axdc4lem  10349  inar1  10669  axdc4uzlem  13890  seqf1olem2  13949  seqf1o  13950  lswco  14746  lo1o1  15439  o1co  15493  caucvgrlem2  15582  summolem3  15621  fsumf1o  15630  fsumcl2lem  15638  fsumadd  15647  fsummulc2  15691  fsumrelem  15714  supcvg  15763  prodmolem3  15840  fprodf1o  15853  fprodser  15856  fprodcl2lem  15857  fprodmul  15867  fproddiv  15868  fprodn0  15886  ruclem11  16149  ruclem12  16150  algcvg  16487  eulerthlem2  16693  cofu1  17791  cofu2  17793  cofucl  17795  fucidcl  17875  fuclid  17876  fucrid  17877  homadm  17947  homacd  17948  evlfcl  18128  curfuncf  18144  yonedalem4c  18183  yonedalem3b  18185  mgmhmco  18588  mhmco  18697  prdspjmhm  18703  pwsco1mhm  18706  lactghmga  19284  frgpup3lem  19656  gsumval3eu  19783  gsumval3  19786  gsumzaddlem  19800  gsumzmhm  19816  dprdf1o  19913  gsumfsum  21341  zrhpsgninv  21492  zrhpsgnevpm  21498  zrhpsgnodpm  21499  evlssca  21994  evls1val  22205  evls1sca  22208  evl1val  22214  mdetralt  22493  mdetunilem7  22503  cpmadumatpoly  22768  chcoeffeqlem  22770  cnpco  23152  lmcnp  23189  upxp  23508  uptx  23510  cnmpt11  23548  cnmpt21  23556  xkofvcn  23569  prdstmdd  24009  prdstgpd  24010  comet  24399  prdsxmslem2  24415  nrmmetd  24460  isngp3  24484  ngpds  24490  tngnm  24537  nmoco  24623  cnmetdval  24656  climcncf  24791  cncfco  24798  htpyco1  24875  htpyco2  24876  phtpyco2  24887  reparphti  24894  reparphtiOLD  24895  copco  24916  pi1cof  24957  pi1coghm  24959  caubl  25206  caublcls  25207  cniccbdd  25360  ovolfioo  25366  ovolficc  25367  ovolfsval  25369  ovolicc2lem1  25416  ovolicc2lem4  25419  ovolicc2lem5  25420  volsup  25455  uniiccdif  25477  uniioovol  25478  uniiccvol  25479  uniioombllem2  25482  uniioombllem3a  25483  uniioombllem4  25485  uniioombllem5  25486  mbfimaopnlem  25554  limccnp  25790  dvcobr  25847  dvcobrOLD  25848  dvcjbr  25851  dvfre  25853  plycjlem  26180  plycj  26181  coecj  26182  plycjOLD  26183  coecjOLD  26184  radcnvlem2  26321  radcnvlem3  26322  radcnvlt2  26326  pserulm  26329  resinf1o  26443  jensen  26897  eflgam  26953  ftalem3  26983  dchrinv  27170  dchr2sum  27182  dchrisum0re  27422  motco  28485  motcgrg  28489  ex-co  30382  vafval  30547  smfval  30549  vsfval  30577  imsdval  30630  lnocoi  30701  occllem  31247  hocoi  31708  homco1  31745  counop  31865  homco2  31921  hmopco  31967  nlelchi  32005  kbass2  32061  kbass5  32064  leopsq  32073  hmopidmchi  32095  elpjrn  32134  pjinvari  32135  cycpmco2  33075  derangenlem  35148  subfacp1lem5  35161  cnpconn  35207  txsconnlem  35217  txsconn  35218  cvmliftmolem1  35258  cvmliftlem7  35268  cvmlift2lem3  35282  cvmlift2lem7  35286  cvmlift2lem9  35288  cvmliftphtlem  35294  cvmlift3lem1  35296  cvmlift3lem2  35297  cvmlift3lem4  35299  cvmlift3lem5  35300  cvmlift3lem6  35301  cvmlift3lem7  35302  mrsubco  35498  msubco  35508  mclsppslem  35560  sinccvglem  35649  iprodefisumlem  35717  iprodefisum  35718  poimirlem22  37626  mblfinlem2  37642  ftc1anclem5  37681  ftc1anclem8  37684  cocanfo  37703  f1ocan1fv  37710  upixp  37713  ghomco  37875  rngohomco  37958  lautco  40080  ldilco  40099  ltrncoval  40128  tendocoval  40749  tendoconid  40812  tendospass  41002  dicvscacl  41174  cdlemn3  41180  cdlemn9  41188  brcoffn  44007  fvovco  45175  climexp  45590  stoweidlem27  46012  stoweidlem31  46016  ovolval4lem1  46634  gricushgr  47905  uspgrlimlem3  47978  uspgrlimlem4  47979  grlictr  48003