Theorem fvco3 6185

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ∘ ccom 5042   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812

This theorem is referenced by:  foco2  6287  foco2OLD  6288  f1ocnvfv1  6432  f1ocnvfv2  6433  fcof1  6442  fcofo  6443  cocan1  6446  cocan2  6447  fveqf1o  6457  isotr  6486  algrflem  7173  fipreima  8155  fsuppco2  8191  fsuppcor  8192  unxpwdom2  8376  wemapwe  8477  ackbij2lem2  8945  cofsmo  8974  cfcoflem  8977  isf32lem6  9063  isf32lem7  9064  isf32lem8  9065  isf34lem7  9084  isf34lem6  9085  axcc3  9143  axdc4lem  9160  canthp1lem2  9354  inar1  9476  axdc4uzlem  12644  seqf1olem2  12703  seqf1o  12704  lswco  13435  lo1o1  14111  o1co  14165  caucvgrlem2  14253  summolem3  14292  fsumf1o  14301  fsumcl2lem  14309  fsumadd  14317  fsummulc2  14358  fsumrelem  14380  supcvg  14427  prodmolem3  14502  fprodf1o  14515  fprodser  14518  fprodcl2lem  14519  fprodmul  14529  fproddiv  14530  fprodn0  14548  ruclem11  14808  ruclem12  14809  algcvg  15127  eulerthlem2  15325  cofu1  16367  cofu2  16369  cofucl  16371  fucidcl  16448  fuclid  16449  fucrid  16450  homadm  16513  homacd  16514  evlfcl  16685  curfuncf  16701  yonedalem4c  16740  yonedalem3b  16742  yonedainv  16744  mhmco  17185  prdspjmhm  17190  pwsco1mhm  17193  lactghmga  17647  frgpup3lem  18013  gsumval3eu  18128  gsumval3  18131  gsumzaddlem  18144  gsumzmhm  18160  dprdf1o  18254  mplsubglem  19255  evlssca  19343  evls1val  19506  evls1sca  19509  evl1val  19514  gsumfsum  19632  frgpcyg  19741  zrhpsgninv  19750  zrhpsgnevpm  19756  zrhpsgnodpm  19757  mdetralt  20233  mdetunilem7  20243  cpmadumatpoly  20507  chcoeffeqlem  20509  cnpco  20881  lmcnp  20918  upxp  21236  uptx  21238  cnmpt11  21276  cnmpt21  21284  xkofvcn  21297  prdstmdd  21737  prdstgpd  21738  comet  22128  prdsxmslem2  22144  nrmmetd  22189  isngp3  22212  ngpds  22218  tngnm  22265  nmoco  22351  cnmetdval  22384  climcncf  22511  cncfco  22518  htpyco1  22585  htpyco2  22586  phtpyco2  22597  reparphti  22605  copco  22626  pi1cof  22667  pi1coghm  22669  caubl  22914  caublcls  22915  cniccbdd  23037  ovolfioo  23043  ovolficc  23044  ovolfsval  23046  ovolicc2lem1  23092  ovolicc2lem4  23095  ovolicc2lem5  23096  volsup  23131  uniiccdif  23152  uniioovol  23153  uniiccvol  23154  uniioombllem2  23157  uniioombllem3a  23158  uniioombllem4  23160  uniioombllem5  23161  mbfimaopnlem  23228  limccnp  23461  dvcobr  23515  dvcjbr  23518  dvfre  23520  plycjlem  23836  plycj  23837  coecj  23838  radcnvlem2  23972  radcnvlem3  23973  radcnvlt2  23977  pserulm  23980  resinf1o  24086  jensen  24515  eflgam  24571  ftalem3  24601  dchrinv  24786  dchr2sum  24798  dchrisum0re  25002  motco  25235  motcgrg  25239  ex-co  26687  vafval  26842  smfval  26844  vsfval  26872  imsdval  26925  lnocoi  26996  occllem  27546  hocoi  28007  homco1  28044  counop  28164  homco2  28220  hmopco  28266  nlelchi  28304  kbass2  28360  kbass5  28363  leopsq  28372  hmopidmchi  28394  elpjrn  28433  pjinvari  28434  derangenlem  30407  subfacp1lem5  30420  cnpcon  30466  txsconlem  30476  txscon  30477  cvmliftmolem1  30517  cvmliftlem7  30527  cvmlift2lem3  30541  cvmlift2lem7  30545  cvmlift2lem9  30547  cvmliftphtlem  30553  cvmlift3lem1  30555  cvmlift3lem2  30556  cvmlift3lem4  30558  cvmlift3lem5  30559  cvmlift3lem6  30560  cvmlift3lem7  30561  mrsubco  30672  msubco  30682  mclsppslem  30734  sinccvglem  30820  iprodefisumlem  30879  iprodefisum  30880  poimirlem22  32601  mblfinlem2  32617  ftc1anclem5  32659  ftc1anclem8  32662  cocanfo  32682  f1ocan1fv  32691  upixp  32694  ghomco  32860  rngohomco  32943  lautco  34401  ldilco  34420  ltrncoval  34449  tendocoval  35072  tendoconid  35135  tendospass  35326  dicvscacl  35498  cdlemn3  35504  cdlemn9  35512  brcoffn  37348  fvco3d  37484  fvovco  38376  climexp  38672  stoweidlem27  38920  stoweidlem31  38924  ovolval4lem1  39539  f1cofveqaeqALT  40324  mgmhmco  41591