Theorem fvco3 6931

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ∘ ccom 5626   Fn wfn 6485  ⟶wf 6486  ‘cfv 6490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-fv 6498

This theorem is referenced by:  fvco3d  6932  foco2  7052  f1cofveqaeqALT  7202  f1ocnvfv1  7220  f1ocnvfv2  7221  fcof1  7231  fcofo  7232  cocan1  7235  cocan2  7236  fveqf1o  7246  isotr  7280  fipreima  9256  fsuppco2  9304  fsuppcor  9305  unxpwdom2  9491  wemapwe  9604  ackbij2lem2  10147  cofsmo  10177  cfcoflem  10180  isf32lem6  10266  isf32lem7  10267  isf32lem8  10268  isf34lem7  10287  isf34lem6  10288  axcc3  10346  axdc4lem  10363  inar1  10684  axdc4uzlem  13904  seqf1olem2  13963  seqf1o  13964  lswco  14760  lo1o1  15453  o1co  15507  caucvgrlem2  15596  summolem3  15635  fsumf1o  15644  fsumcl2lem  15652  fsumadd  15661  fsummulc2  15705  fsumrelem  15728  supcvg  15777  prodmolem3  15854  fprodf1o  15867  fprodser  15870  fprodcl2lem  15871  fprodmul  15881  fproddiv  15882  fprodn0  15900  ruclem11  16163  ruclem12  16164  algcvg  16501  eulerthlem2  16707  cofu1  17806  cofu2  17808  cofucl  17810  fucidcl  17890  fuclid  17891  fucrid  17892  homadm  17962  homacd  17963  evlfcl  18143  curfuncf  18159  yonedalem4c  18198  yonedalem3b  18200  mgmhmco  18637  mhmco  18746  prdspjmhm  18752  pwsco1mhm  18755  lactghmga  19332  frgpup3lem  19704  gsumval3eu  19831  gsumval3  19834  gsumzaddlem  19848  gsumzmhm  19864  dprdf1o  19961  gsumfsum  21387  zrhpsgninv  21538  zrhpsgnevpm  21544  zrhpsgnodpm  21545  evlssca  22047  evls1val  22262  evls1sca  22265  evl1val  22271  mdetralt  22550  mdetunilem7  22560  cpmadumatpoly  22825  chcoeffeqlem  22827  cnpco  23209  lmcnp  23246  upxp  23565  uptx  23567  cnmpt11  23605  cnmpt21  23613  xkofvcn  23626  prdstmdd  24066  prdstgpd  24067  comet  24455  prdsxmslem2  24471  nrmmetd  24516  isngp3  24540  ngpds  24546  tngnm  24593  nmoco  24679  cnmetdval  24712  climcncf  24847  cncfco  24854  htpyco1  24931  htpyco2  24932  phtpyco2  24943  reparphti  24950  reparphtiOLD  24951  copco  24972  pi1cof  25013  pi1coghm  25015  caubl  25262  caublcls  25263  cniccbdd  25416  ovolfioo  25422  ovolficc  25423  ovolfsval  25425  ovolicc2lem1  25472  ovolicc2lem4  25475  ovolicc2lem5  25476  volsup  25511  uniiccdif  25533  uniioovol  25534  uniiccvol  25535  uniioombllem2  25538  uniioombllem3a  25539  uniioombllem4  25541  uniioombllem5  25542  mbfimaopnlem  25610  limccnp  25846  dvcobr  25903  dvcobrOLD  25904  dvcjbr  25907  dvfre  25909  plycjlem  26236  plycj  26237  coecj  26238  plycjOLD  26239  coecjOLD  26240  radcnvlem2  26377  radcnvlem3  26378  radcnvlt2  26382  pserulm  26385  resinf1o  26499  jensen  26953  eflgam  27009  ftalem3  27039  dchrinv  27226  dchr2sum  27238  dchrisum0re  27478  motco  28561  motcgrg  28565  ex-co  30462  vafval  30627  smfval  30629  vsfval  30657  imsdval  30710  lnocoi  30781  occllem  31327  hocoi  31788  homco1  31825  counop  31945  homco2  32001  hmopco  32047  nlelchi  32085  kbass2  32141  kbass5  32144  leopsq  32153  hmopidmchi  32175  elpjrn  32214  pjinvari  32215  cycpmco2  33164  derangenlem  35314  subfacp1lem5  35327  cnpconn  35373  txsconnlem  35383  txsconn  35384  cvmliftmolem1  35424  cvmliftlem7  35434  cvmlift2lem3  35448  cvmlift2lem7  35452  cvmlift2lem9  35454  cvmliftphtlem  35460  cvmlift3lem1  35462  cvmlift3lem2  35463  cvmlift3lem4  35465  cvmlift3lem5  35466  cvmlift3lem6  35467  cvmlift3lem7  35468  mrsubco  35664  msubco  35674  mclsppslem  35726  sinccvglem  35815  iprodefisumlem  35883  iprodefisum  35884  poimirlem22  37782  mblfinlem2  37798  ftc1anclem5  37837  ftc1anclem8  37840  cocanfo  37859  f1ocan1fv  37866  upixp  37869  ghomco  38031  rngohomco  38114  lautco  40296  ldilco  40315  ltrncoval  40344  tendocoval  40965  tendoconid  41028  tendospass  41218  dicvscacl  41390  cdlemn3  41396  cdlemn9  41404  brcoffn  44213  fvovco  45379  climexp  45793  stoweidlem27  46213  stoweidlem31  46217  ovolval4lem1  46835  gricushgr  48105  uspgrlimlem3  48178  uspgrlimlem4  48179  grlictr  48203