Theorem fvco3 6985

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107   ∘ ccom 5678   Fn wfn 6534  ⟶wf 6535  ‘cfv 6539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5297  ax-nul 5304  ax-pr 5425

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4321  df-if 4527  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4907  df-br 5147  df-opab 5209  df-id 5572  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-iota 6491  df-fun 6541  df-fn 6542  df-f 6543  df-fv 6547

This theorem is referenced by:  fvco3d  6986  foco2  7103  f1cofveqaeqALT  7252  f1ocnvfv1  7268  f1ocnvfv2  7269  fcof1  7279  fcofo  7280  cocan1  7283  cocan2  7284  fveqf1o  7295  isotr  7327  fipreima  9353  fsuppco2  9393  fsuppcor  9394  unxpwdom2  9578  wemapwe  9687  ackbij2lem2  10230  cofsmo  10259  cfcoflem  10262  isf32lem6  10348  isf32lem7  10349  isf32lem8  10350  isf34lem7  10369  isf34lem6  10370  axcc3  10428  axdc4lem  10445  inar1  10765  axdc4uzlem  13943  seqf1olem2  14003  seqf1o  14004  lswco  14785  lo1o1  15471  o1co  15525  caucvgrlem2  15616  summolem3  15655  fsumf1o  15664  fsumcl2lem  15672  fsumadd  15681  fsummulc2  15725  fsumrelem  15748  supcvg  15797  prodmolem3  15872  fprodf1o  15885  fprodser  15888  fprodcl2lem  15889  fprodmul  15899  fproddiv  15900  fprodn0  15918  ruclem11  16178  ruclem12  16179  algcvg  16508  eulerthlem2  16710  cofu1  17829  cofu2  17831  cofucl  17833  fucidcl  17913  fuclid  17914  fucrid  17915  homadm  17985  homacd  17986  evlfcl  18170  curfuncf  18186  yonedalem4c  18225  yonedalem3b  18227  mhmco  18699  prdspjmhm  18705  pwsco1mhm  18708  lactghmga  19265  frgpup3lem  19637  gsumval3eu  19763  gsumval3  19766  gsumzaddlem  19780  gsumzmhm  19796  dprdf1o  19893  gsumfsum  20996  zrhpsgninv  21121  zrhpsgnevpm  21127  zrhpsgnodpm  21128  evlssca  21633  evls1val  21820  evls1sca  21823  evl1val  21829  mdetralt  22091  mdetunilem7  22101  cpmadumatpoly  22366  chcoeffeqlem  22368  cnpco  22752  lmcnp  22789  upxp  23108  uptx  23110  cnmpt11  23148  cnmpt21  23156  xkofvcn  23169  prdstmdd  23609  prdstgpd  23610  comet  24003  prdsxmslem2  24019  nrmmetd  24064  isngp3  24088  ngpds  24094  tngnm  24149  nmoco  24235  cnmetdval  24268  climcncf  24397  cncfco  24404  htpyco1  24475  htpyco2  24476  phtpyco2  24487  reparphti  24494  copco  24515  pi1cof  24556  pi1coghm  24558  caubl  24806  caublcls  24807  cniccbdd  24959  ovolfioo  24965  ovolficc  24966  ovolfsval  24968  ovolicc2lem1  25015  ovolicc2lem4  25018  ovolicc2lem5  25019  volsup  25054  uniiccdif  25076  uniioovol  25077  uniiccvol  25078  uniioombllem2  25081  uniioombllem3a  25082  uniioombllem4  25084  uniioombllem5  25085  mbfimaopnlem  25153  limccnp  25389  dvcobr  25444  dvcjbr  25447  dvfre  25449  plycjlem  25771  plycj  25772  coecj  25773  radcnvlem2  25907  radcnvlem3  25908  radcnvlt2  25912  pserulm  25915  resinf1o  26026  jensen  26472  eflgam  26528  ftalem3  26558  dchrinv  26743  dchr2sum  26755  dchrisum0re  26995  motco  27770  motcgrg  27774  ex-co  29670  vafval  29833  smfval  29835  vsfval  29863  imsdval  29916  lnocoi  29987  occllem  30533  hocoi  30994  homco1  31031  counop  31151  homco2  31207  hmopco  31253  nlelchi  31291  kbass2  31347  kbass5  31350  leopsq  31359  hmopidmchi  31381  elpjrn  31420  pjinvari  31421  cycpmco2  32269  derangenlem  34099  subfacp1lem5  34112  cnpconn  34158  txsconnlem  34168  txsconn  34169  cvmliftmolem1  34209  cvmliftlem7  34219  cvmlift2lem3  34233  cvmlift2lem7  34237  cvmlift2lem9  34239  cvmliftphtlem  34245  cvmlift3lem1  34247  cvmlift3lem2  34248  cvmlift3lem4  34250  cvmlift3lem5  34251  cvmlift3lem6  34252  cvmlift3lem7  34253  mrsubco  34449  msubco  34459  mclsppslem  34511  sinccvglem  34594  iprodefisumlem  34647  iprodefisum  34648  gg-reparphti  35109  gg-dvcobr  35113  poimirlem22  36447  mblfinlem2  36463  ftc1anclem5  36502  ftc1anclem8  36505  cocanfo  36524  f1ocan1fv  36531  upixp  36534  ghomco  36696  rngohomco  36779  lautco  38905  ldilco  38924  ltrncoval  38953  tendocoval  39574  tendoconid  39637  tendospass  39827  dicvscacl  39999  cdlemn3  40005  cdlemn9  40013  brcoffn  42713  fvovco  43824  climexp  44255  stoweidlem27  44677  stoweidlem31  44681  ovolval4lem1  45299  isomushgr  46428  mgmhmco  46505