Theorem fvco3 6810

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ∈ wcel 2110   ∘ ccom 5555   Fn wfn 6375  ⟶wf 6376  ‘cfv 6380

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-fv 6388

This theorem is referenced by:  fvco3d  6811  foco2  6926  f1cofveqaeqALT  7071  f1ocnvfv1  7087  f1ocnvfv2  7088  fcof1  7097  fcofo  7098  cocan1  7101  cocan2  7102  fveqf1o  7113  isotr  7145  algrflem  7892  fipreima  8982  fsuppco2  9019  fsuppcor  9020  unxpwdom2  9204  wemapwe  9312  ackbij2lem2  9854  cofsmo  9883  cfcoflem  9886  isf32lem6  9972  isf32lem7  9973  isf32lem8  9974  isf34lem7  9993  isf34lem6  9994  axcc3  10052  axdc4lem  10069  inar1  10389  axdc4uzlem  13556  seqf1olem2  13616  seqf1o  13617  lswco  14404  lo1o1  15093  o1co  15147  caucvgrlem2  15238  summolem3  15278  fsumf1o  15287  fsumcl2lem  15295  fsumadd  15304  fsummulc2  15348  fsumrelem  15371  supcvg  15420  prodmolem3  15495  fprodf1o  15508  fprodser  15511  fprodcl2lem  15512  fprodmul  15522  fproddiv  15523  fprodn0  15541  ruclem11  15801  ruclem12  15802  algcvg  16133  eulerthlem2  16335  cofu1  17390  cofu2  17392  cofucl  17394  fucidcl  17474  fuclid  17475  fucrid  17476  homadm  17546  homacd  17547  evlfcl  17730  curfuncf  17746  yonedalem4c  17785  yonedalem3b  17787  mhmco  18250  prdspjmhm  18255  pwsco1mhm  18258  lactghmga  18797  frgpup3lem  19167  gsumval3eu  19289  gsumval3  19292  gsumzaddlem  19306  gsumzmhm  19322  dprdf1o  19419  gsumfsum  20430  zrhpsgninv  20547  zrhpsgnevpm  20553  zrhpsgnodpm  20554  evlssca  21049  evls1val  21236  evls1sca  21239  evl1val  21245  mdetralt  21505  mdetunilem7  21515  cpmadumatpoly  21780  chcoeffeqlem  21782  cnpco  22164  lmcnp  22201  upxp  22520  uptx  22522  cnmpt11  22560  cnmpt21  22568  xkofvcn  22581  prdstmdd  23021  prdstgpd  23022  comet  23411  prdsxmslem2  23427  nrmmetd  23472  isngp3  23496  ngpds  23502  tngnm  23549  nmoco  23635  cnmetdval  23668  climcncf  23797  cncfco  23804  htpyco1  23875  htpyco2  23876  phtpyco2  23887  reparphti  23894  copco  23915  pi1cof  23956  pi1coghm  23958  caubl  24205  caublcls  24206  cniccbdd  24358  ovolfioo  24364  ovolficc  24365  ovolfsval  24367  ovolicc2lem1  24414  ovolicc2lem4  24417  ovolicc2lem5  24418  volsup  24453  uniiccdif  24475  uniioovol  24476  uniiccvol  24477  uniioombllem2  24480  uniioombllem3a  24481  uniioombllem4  24483  uniioombllem5  24484  mbfimaopnlem  24552  limccnp  24788  dvcobr  24843  dvcjbr  24846  dvfre  24848  plycjlem  25170  plycj  25171  coecj  25172  radcnvlem2  25306  radcnvlem3  25307  radcnvlt2  25311  pserulm  25314  resinf1o  25425  jensen  25871  eflgam  25927  ftalem3  25957  dchrinv  26142  dchr2sum  26154  dchrisum0re  26394  motco  26631  motcgrg  26635  ex-co  28521  vafval  28684  smfval  28686  vsfval  28714  imsdval  28767  lnocoi  28838  occllem  29384  hocoi  29845  homco1  29882  counop  30002  homco2  30058  hmopco  30104  nlelchi  30142  kbass2  30198  kbass5  30201  leopsq  30210  hmopidmchi  30232  elpjrn  30271  pjinvari  30272  cycpmco2  31119  derangenlem  32846  subfacp1lem5  32859  cnpconn  32905  txsconnlem  32915  txsconn  32916  cvmliftmolem1  32956  cvmliftlem7  32966  cvmlift2lem3  32980  cvmlift2lem7  32984  cvmlift2lem9  32986  cvmliftphtlem  32992  cvmlift3lem1  32994  cvmlift3lem2  32995  cvmlift3lem4  32997  cvmlift3lem5  32998  cvmlift3lem6  32999  cvmlift3lem7  33000  mrsubco  33196  msubco  33206  mclsppslem  33258  sinccvglem  33343  iprodefisumlem  33424  iprodefisum  33425  poimirlem22  35536  mblfinlem2  35552  ftc1anclem5  35591  ftc1anclem8  35594  cocanfo  35613  f1ocan1fv  35621  upixp  35624  ghomco  35786  rngohomco  35869  lautco  37848  ldilco  37867  ltrncoval  37896  tendocoval  38517  tendoconid  38580  tendospass  38770  dicvscacl  38942  cdlemn3  38948  cdlemn9  38956  brcoffn  41317  fvovco  42405  climexp  42821  stoweidlem27  43243  stoweidlem31  43247  ovolval4lem1  43862  isomushgr  44951  mgmhmco  45028