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  17822  cofu2  17824  cofucl  17826  fucidcl  17906  fuclid  17907  fucrid  17908  homadm  17978  homacd  17979  evlfcl  18159  curfuncf  18175  yonedalem4c  18214  yonedalem3b  18216  mgmhmco  18617  mhmco  18726  prdspjmhm  18732  pwsco1mhm  18735  lactghmga  19311  frgpup3lem  19683  gsumval3eu  19810  gsumval3  19813  gsumzaddlem  19827  gsumzmhm  19843  dprdf1o  19940  gsumfsum  21327  zrhpsgninv  21470  zrhpsgnevpm  21476  zrhpsgnodpm  21477  evlssca  21972  evls1val  22183  evls1sca  22186  evl1val  22192  mdetralt  22471  mdetunilem7  22481  cpmadumatpoly  22746  chcoeffeqlem  22748  cnpco  23130  lmcnp  23167  upxp  23486  uptx  23488  cnmpt11  23526  cnmpt21  23534  xkofvcn  23547  prdstmdd  23987  prdstgpd  23988  comet  24377  prdsxmslem2  24393  nrmmetd  24438  isngp3  24462  ngpds  24468  tngnm  24515  nmoco  24601  cnmetdval  24634  climcncf  24769  cncfco  24776  htpyco1  24853  htpyco2  24854  phtpyco2  24865  reparphti  24872  reparphtiOLD  24873  copco  24894  pi1cof  24935  pi1coghm  24937  caubl  25184  caublcls  25185  cniccbdd  25338  ovolfioo  25344  ovolficc  25345  ovolfsval  25347  ovolicc2lem1  25394  ovolicc2lem4  25397  ovolicc2lem5  25398  volsup  25433  uniiccdif  25455  uniioovol  25456  uniiccvol  25457  uniioombllem2  25460  uniioombllem3a  25461  uniioombllem4  25463  uniioombllem5  25464  mbfimaopnlem  25532  limccnp  25768  dvcobr  25825  dvcobrOLD  25826  dvcjbr  25829  dvfre  25831  plycjlem  26158  plycj  26159  coecj  26160  plycjOLD  26161  coecjOLD  26162  radcnvlem2  26299  radcnvlem3  26300  radcnvlt2  26304  pserulm  26307  resinf1o  26421  jensen  26875  eflgam  26931  ftalem3  26961  dchrinv  27148  dchr2sum  27160  dchrisum0re  27400  motco  28443  motcgrg  28447  ex-co  30340  vafval  30505  smfval  30507  vsfval  30535  imsdval  30588  lnocoi  30659  occllem  31205  hocoi  31666  homco1  31703  counop  31823  homco2  31879  hmopco  31925  nlelchi  31963  kbass2  32019  kbass5  32022  leopsq  32031  hmopidmchi  32053  elpjrn  32092  pjinvari  32093  cycpmco2  33063  derangenlem  35131  subfacp1lem5  35144  cnpconn  35190  txsconnlem  35200  txsconn  35201  cvmliftmolem1  35241  cvmliftlem7  35251  cvmlift2lem3  35265  cvmlift2lem7  35269  cvmlift2lem9  35271  cvmliftphtlem  35277  cvmlift3lem1  35279  cvmlift3lem2  35280  cvmlift3lem4  35282  cvmlift3lem5  35283  cvmlift3lem6  35284  cvmlift3lem7  35285  mrsubco  35481  msubco  35491  mclsppslem  35543  sinccvglem  35632  iprodefisumlem  35700  iprodefisum  35701  poimirlem22  37609  mblfinlem2  37625  ftc1anclem5  37664  ftc1anclem8  37667  cocanfo  37686  f1ocan1fv  37693  upixp  37696  ghomco  37858  rngohomco  37941  lautco  40064  ldilco  40083  ltrncoval  40112  tendocoval  40733  tendoconid  40796  tendospass  40986  dicvscacl  41158  cdlemn3  41164  cdlemn9  41172  brcoffn  43992  fvovco  45160  climexp  45576  stoweidlem27  45998  stoweidlem31  46002  ovolval4lem1  46620  gricushgr  47890  uspgrlimlem3  47962  uspgrlimlem4  47963  grlictr  47980