Theorem fvco3 6934

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ∘ ccom 5629   Fn wfn 6488  ⟶wf 6489  ‘cfv 6493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501

This theorem is referenced by:  fvco3d  6935  foco2  7056  f1cofveqaeqALT  7207  f1ocnvfv1  7225  f1ocnvfv2  7226  fcof1  7236  fcofo  7237  cocan1  7240  cocan2  7241  fveqf1o  7251  isotr  7285  fipreima  9262  fsuppco2  9310  fsuppcor  9311  unxpwdom2  9497  wemapwe  9612  ackbij2lem2  10155  cofsmo  10185  cfcoflem  10188  isf32lem6  10274  isf32lem7  10275  isf32lem8  10276  isf34lem7  10295  isf34lem6  10296  axcc3  10354  axdc4lem  10371  inar1  10692  axdc4uzlem  13939  seqf1olem2  13998  seqf1o  13999  lswco  14795  lo1o1  15488  o1co  15542  caucvgrlem2  15631  summolem3  15670  fsumf1o  15679  fsumcl2lem  15687  fsumadd  15696  fsummulc2  15740  fsumrelem  15764  supcvg  15815  prodmolem3  15892  fprodf1o  15905  fprodser  15908  fprodcl2lem  15909  fprodmul  15919  fproddiv  15920  fprodn0  15938  ruclem11  16201  ruclem12  16202  algcvg  16539  eulerthlem2  16746  cofu1  17845  cofu2  17847  cofucl  17849  fucidcl  17929  fuclid  17930  fucrid  17931  homadm  18001  homacd  18002  evlfcl  18182  curfuncf  18198  yonedalem4c  18237  yonedalem3b  18239  mgmhmco  18676  mhmco  18785  prdspjmhm  18791  pwsco1mhm  18794  lactghmga  19374  frgpup3lem  19746  gsumval3eu  19873  gsumval3  19876  gsumzaddlem  19890  gsumzmhm  19906  dprdf1o  20003  gsumfsum  21427  zrhpsgninv  21578  zrhpsgnevpm  21584  zrhpsgnodpm  21585  evlssca  22085  evls1val  22298  evls1sca  22301  evl1val  22307  mdetralt  22586  mdetunilem7  22596  cpmadumatpoly  22861  chcoeffeqlem  22863  cnpco  23245  lmcnp  23282  upxp  23601  uptx  23603  cnmpt11  23641  cnmpt21  23649  xkofvcn  23662  prdstmdd  24102  prdstgpd  24103  comet  24491  prdsxmslem2  24507  nrmmetd  24552  isngp3  24576  ngpds  24582  tngnm  24629  nmoco  24715  cnmetdval  24748  climcncf  24880  cncfco  24887  htpyco1  24958  htpyco2  24959  phtpyco2  24970  reparphti  24977  copco  24998  pi1cof  25039  pi1coghm  25041  caubl  25288  caublcls  25289  cniccbdd  25441  ovolfioo  25447  ovolficc  25448  ovolfsval  25450  ovolicc2lem1  25497  ovolicc2lem4  25500  ovolicc2lem5  25501  volsup  25536  uniiccdif  25558  uniioovol  25559  uniiccvol  25560  uniioombllem2  25563  uniioombllem3a  25564  uniioombllem4  25566  uniioombllem5  25567  mbfimaopnlem  25635  limccnp  25871  dvcobr  25926  dvcjbr  25929  dvfre  25931  plycjlem  26254  plycj  26255  coecj  26256  plycjOLD  26257  coecjOLD  26258  radcnvlem2  26395  radcnvlem3  26396  radcnvlt2  26400  pserulm  26403  resinf1o  26516  jensen  26969  eflgam  27025  ftalem3  27055  dchrinv  27241  dchr2sum  27253  dchrisum0re  27493  motco  28625  motcgrg  28629  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  33212  derangenlem  35372  subfacp1lem5  35385  cnpconn  35431  txsconnlem  35441  txsconn  35442  cvmliftmolem1  35482  cvmliftlem7  35492  cvmlift2lem3  35506  cvmlift2lem7  35510  cvmlift2lem9  35512  cvmliftphtlem  35518  cvmlift3lem1  35520  cvmlift3lem2  35521  cvmlift3lem4  35523  cvmlift3lem5  35524  cvmlift3lem6  35525  cvmlift3lem7  35526  mrsubco  35722  msubco  35732  mclsppslem  35784  sinccvglem  35873  iprodefisumlem  35941  iprodefisum  35942  poimirlem22  37980  mblfinlem2  37996  ftc1anclem5  38035  ftc1anclem8  38038  cocanfo  38057  f1ocan1fv  38064  upixp  38067  ghomco  38229  rngohomco  38312  lautco  40560  ldilco  40579  ltrncoval  40608  tendocoval  41229  tendoconid  41292  tendospass  41482  dicvscacl  41654  cdlemn3  41660  cdlemn9  41668  brcoffn  44478  fvovco  45644  climexp  46056  stoweidlem27  46476  stoweidlem31  46480  ovolval4lem1  47098  gricushgr  48408  uspgrlimlem3  48481  uspgrlimlem4  48482  grlictr  48506