Theorem fvco3 6942

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ∘ ccom 5635   Fn wfn 6494  ⟶wf 6495  ‘cfv 6499

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-fv 6507

This theorem is referenced by:  fvco3d  6943  foco2  7063  f1cofveqaeqALT  7215  f1ocnvfv1  7233  f1ocnvfv2  7234  fcof1  7244  fcofo  7245  cocan1  7248  cocan2  7249  fveqf1o  7259  isotr  7293  fipreima  9285  fsuppco2  9330  fsuppcor  9331  unxpwdom2  9517  wemapwe  9626  ackbij2lem2  10168  cofsmo  10198  cfcoflem  10201  isf32lem6  10287  isf32lem7  10288  isf32lem8  10289  isf34lem7  10308  isf34lem6  10309  axcc3  10367  axdc4lem  10384  inar1  10704  axdc4uzlem  13924  seqf1olem2  13983  seqf1o  13984  lswco  14781  lo1o1  15474  o1co  15528  caucvgrlem2  15617  summolem3  15656  fsumf1o  15665  fsumcl2lem  15673  fsumadd  15682  fsummulc2  15726  fsumrelem  15749  supcvg  15798  prodmolem3  15875  fprodf1o  15888  fprodser  15891  fprodcl2lem  15892  fprodmul  15902  fproddiv  15903  fprodn0  15921  ruclem11  16184  ruclem12  16185  algcvg  16522  eulerthlem2  16728  cofu1  17826  cofu2  17828  cofucl  17830  fucidcl  17910  fuclid  17911  fucrid  17912  homadm  17982  homacd  17983  evlfcl  18163  curfuncf  18179  yonedalem4c  18218  yonedalem3b  18220  mgmhmco  18623  mhmco  18732  prdspjmhm  18738  pwsco1mhm  18741  lactghmga  19319  frgpup3lem  19691  gsumval3eu  19818  gsumval3  19821  gsumzaddlem  19835  gsumzmhm  19851  dprdf1o  19948  gsumfsum  21376  zrhpsgninv  21527  zrhpsgnevpm  21533  zrhpsgnodpm  21534  evlssca  22029  evls1val  22240  evls1sca  22243  evl1val  22249  mdetralt  22528  mdetunilem7  22538  cpmadumatpoly  22803  chcoeffeqlem  22805  cnpco  23187  lmcnp  23224  upxp  23543  uptx  23545  cnmpt11  23583  cnmpt21  23591  xkofvcn  23604  prdstmdd  24044  prdstgpd  24045  comet  24434  prdsxmslem2  24450  nrmmetd  24495  isngp3  24519  ngpds  24525  tngnm  24572  nmoco  24658  cnmetdval  24691  climcncf  24826  cncfco  24833  htpyco1  24910  htpyco2  24911  phtpyco2  24922  reparphti  24929  reparphtiOLD  24930  copco  24951  pi1cof  24992  pi1coghm  24994  caubl  25241  caublcls  25242  cniccbdd  25395  ovolfioo  25401  ovolficc  25402  ovolfsval  25404  ovolicc2lem1  25451  ovolicc2lem4  25454  ovolicc2lem5  25455  volsup  25490  uniiccdif  25512  uniioovol  25513  uniiccvol  25514  uniioombllem2  25517  uniioombllem3a  25518  uniioombllem4  25520  uniioombllem5  25521  mbfimaopnlem  25589  limccnp  25825  dvcobr  25882  dvcobrOLD  25883  dvcjbr  25886  dvfre  25888  plycjlem  26215  plycj  26216  coecj  26217  plycjOLD  26218  coecjOLD  26219  radcnvlem2  26356  radcnvlem3  26357  radcnvlt2  26361  pserulm  26364  resinf1o  26478  jensen  26932  eflgam  26988  ftalem3  27018  dchrinv  27205  dchr2sum  27217  dchrisum0re  27457  motco  28520  motcgrg  28524  ex-co  30417  vafval  30582  smfval  30584  vsfval  30612  imsdval  30665  lnocoi  30736  occllem  31282  hocoi  31743  homco1  31780  counop  31900  homco2  31956  hmopco  32002  nlelchi  32040  kbass2  32096  kbass5  32099  leopsq  32108  hmopidmchi  32130  elpjrn  32169  pjinvari  32170  cycpmco2  33105  derangenlem  35151  subfacp1lem5  35164  cnpconn  35210  txsconnlem  35220  txsconn  35221  cvmliftmolem1  35261  cvmliftlem7  35271  cvmlift2lem3  35285  cvmlift2lem7  35289  cvmlift2lem9  35291  cvmliftphtlem  35297  cvmlift3lem1  35299  cvmlift3lem2  35300  cvmlift3lem4  35302  cvmlift3lem5  35303  cvmlift3lem6  35304  cvmlift3lem7  35305  mrsubco  35501  msubco  35511  mclsppslem  35563  sinccvglem  35652  iprodefisumlem  35720  iprodefisum  35721  poimirlem22  37629  mblfinlem2  37645  ftc1anclem5  37684  ftc1anclem8  37687  cocanfo  37706  f1ocan1fv  37713  upixp  37716  ghomco  37878  rngohomco  37961  lautco  40084  ldilco  40103  ltrncoval  40132  tendocoval  40753  tendoconid  40816  tendospass  41006  dicvscacl  41178  cdlemn3  41184  cdlemn9  41192  brcoffn  44012  fvovco  45180  climexp  45596  stoweidlem27  46018  stoweidlem31  46022  ovolval4lem1  46640  gricushgr  47910  uspgrlimlem3  47982  uspgrlimlem4  47983  grlictr  48000