Theorem fvco3 6927

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119   ∘ ccom 5622   Fn wfn 6480  ⟶wf 6481  ‘cfv 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-fv 6493

This theorem is referenced by:  fvco3d  6928  foco2  7050  f1cofveqaeqALT  7202  f1ocnvfv1  7220  f1ocnvfv2  7221  fcof1  7231  fcofo  7232  cocan1  7235  cocan2  7236  fveqf1o  7246  isotr  7280  fipreima  9258  fsuppco2  9306  fsuppcor  9307  unxpwdom2  9493  wemapwe  9609  ackbij2lem2  10152  cofsmo  10182  cfcoflem  10185  isf32lem6  10271  isf32lem7  10272  isf32lem8  10273  isf34lem7  10292  isf34lem6  10293  axcc3  10351  axdc4lem  10368  inar1  10689  axdc4uzlem  13936  seqf1olem2  13995  seqf1o  13996  lswco  14792  lo1o1  15485  o1co  15539  caucvgrlem2  15628  summolem3  15667  fsumf1o  15676  fsumcl2lem  15684  fsumadd  15693  fsummulc2  15737  fsumrelem  15761  supcvg  15812  prodmolem3  15889  fprodf1o  15902  fprodser  15905  fprodcl2lem  15906  fprodmul  15916  fproddiv  15917  fprodn0  15935  ruclem11  16198  ruclem12  16199  algcvg  16536  eulerthlem2  16743  cofu1  17842  cofu2  17844  cofucl  17846  fucidcl  17926  fuclid  17927  fucrid  17928  homadm  17998  homacd  17999  evlfcl  18179  curfuncf  18195  yonedalem4c  18234  yonedalem3b  18236  mgmhmco  18673  mhmco  18782  prdspjmhm  18788  pwsco1mhm  18791  lactghmga  19371  frgpup3lem  19743  gsumval3eu  19870  gsumval3  19873  gsumzaddlem  19887  gsumzmhm  19903  dprdf1o  20000  gsumfsum  21409  zrhpsgninv  21560  zrhpsgnevpm  21566  zrhpsgnodpm  21567  evlssca  22070  evls1val  22306  evls1sca  22309  evl1val  22315  mdetralt  22591  mdetunilem7  22601  cpmadumatpoly  22866  chcoeffeqlem  22868  cnpco  23250  lmcnp  23287  upxp  23606  uptx  23608  cnmpt11  23646  cnmpt21  23654  xkofvcn  23667  prdstmdd  24107  prdstgpd  24108  comet  24496  prdsxmslem2  24512  nrmmetd  24557  isngp3  24581  ngpds  24587  tngnm  24634  nmoco  24720  cnmetdval  24753  climcncf  24885  cncfco  24892  htpyco1  24963  htpyco2  24964  phtpyco2  24975  reparphti  24982  copco  25003  pi1cof  25044  pi1coghm  25046  caubl  25293  caublcls  25294  cniccbdd  25446  ovolfioo  25452  ovolficc  25453  ovolfsval  25455  ovolicc2lem1  25502  ovolicc2lem4  25505  ovolicc2lem5  25506  volsup  25541  uniiccdif  25563  uniioovol  25564  uniiccvol  25565  uniioombllem2  25568  uniioombllem3a  25569  uniioombllem4  25571  uniioombllem5  25572  mbfimaopnlem  25640  limccnp  25876  dvcobr  25931  dvcjbr  25934  dvfre  25936  plycjlem  26259  plycj  26260  coecj  26261  plycjOLD  26262  coecjOLD  26263  radcnvlem2  26397  radcnvlem3  26398  radcnvlt2  26402  pserulm  26405  resinf1o  26518  jensen  26970  eflgam  27026  ftalem3  27056  dchrinv  27242  dchr2sum  27254  dchrisum0re  27494  motco  28626  motcgrg  28630  ex-co  30526  vafval  30692  smfval  30694  vsfval  30722  imsdval  30775  lnocoi  30846  occllem  31392  hocoi  31853  homco1  31890  counop  32010  homco2  32066  hmopco  32112  nlelchi  32150  kbass2  32206  kbass5  32209  leopsq  32218  hmopidmchi  32240  elpjrn  32279  pjinvari  32280  cycpmco2  33214  derangenlem  35399  subfacp1lem5  35412  cnpconn  35458  txsconnlem  35468  txsconn  35469  cvmliftmolem1  35509  cvmliftlem7  35519  cvmlift2lem3  35533  cvmlift2lem7  35537  cvmlift2lem9  35539  cvmliftphtlem  35545  cvmlift3lem1  35547  cvmlift3lem2  35548  cvmlift3lem4  35550  cvmlift3lem5  35551  cvmlift3lem6  35552  cvmlift3lem7  35553  mrsubco  35749  msubco  35759  mclsppslem  35811  sinccvglem  35900  iprodefisumlem  35968  iprodefisum  35969  poimirlem22  38009  mblfinlem2  38025  ftc1anclem5  38064  ftc1anclem8  38067  cocanfo  38086  f1ocan1fv  38093  upixp  38096  ghomco  38258  rngohomco  38341  lautco  40589  ldilco  40608  ltrncoval  40637  tendocoval  41258  tendoconid  41321  tendospass  41511  dicvscacl  41683  cdlemn3  41689  cdlemn9  41697  brcoffn  44474  fvovco  45640  climexp  46050  stoweidlem27  46470  stoweidlem31  46474  ovolval4lem1  47092  gricushgr  48408  uspgrlimlem3  48481  uspgrlimlem4  48482  grlictr  48506