Theorem fvco3 6981

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143   ∘ ccom 5665   Fn wfn 6531  ⟶wf 6532  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544

This theorem is referenced by:  fvco3d  6982  foco2  7104  f1cofveqaeqALT  7256  f1ocnvfv1  7274  f1ocnvfv2  7275  fcof1  7285  fcofo  7286  cocan1  7289  cocan2  7290  fveqf1o  7300  isotr  7334  fipreima  9311  fsuppco2  9359  fsuppcor  9360  unxpwdom2  9546  wemapwe  9662  ackbij2lem2  10218  cofsmo  10248  cfcoflem  10251  isf32lem6  10337  isf32lem7  10338  isf32lem8  10339  isf34lem7  10358  isf34lem6  10359  axcc3  10417  axdc4lem  10434  inar1  10755  axdc4uzlem  14015  seqf1olem2  14074  seqf1o  14075  lswco  14872  lo1o1  15579  o1co  15633  caucvgrlem2  15722  summolem3  15761  fsumf1o  15770  fsumcl2lem  15778  fsumadd  15787  fsummulc2  15831  fsumrelem  15855  supcvg  15906  prodmolem3  15983  fprodf1o  15996  fprodser  15999  fprodcl2lem  16000  fprodmul  16010  fproddiv  16011  fprodn0  16029  ruclem11  16291  ruclem12  16292  algcvg  16629  eulerthlem2  16836  cofu1  17936  cofu2  17938  cofucl  17940  fucidcl  18020  fuclid  18021  fucrid  18022  homadm  18092  homacd  18093  evlfcl  18273  curfuncf  18289  yonedalem4c  18328  yonedalem3b  18330  mgmhmco  18767  mhmco  18877  prdspjmhm  18883  pwsco1mhm  18886  lactghmga  19470  frgpup3lem  19842  gsumval3eu  19969  gsumval3  19972  gsumzaddlem  19986  gsumzmhm  20002  dprdf1o  20099  gsumfsum  21584  zrhpsgninv  21735  zrhpsgnevpm  21741  zrhpsgnodpm  21742  evlssca  22245  evls1val  22480  evls1sca  22483  evl1val  22489  mdetralt  22765  mdetunilem7  22775  cpmadumatpoly  23040  chcoeffeqlem  23042  cnpco  23424  lmcnp  23461  upxp  23780  uptx  23782  cnmpt11  23820  cnmpt21  23828  xkofvcn  23841  prdstmdd  24281  prdstgpd  24282  comet  24670  prdsxmslem2  24686  nrmmetd  24731  isngp3  24755  ngpds  24761  tngnm  24808  nmoco  24894  cnmetdval  24927  climcncf  25059  cncfco  25066  htpyco1  25137  htpyco2  25138  phtpyco2  25149  reparphti  25156  copco  25177  pi1cof  25218  pi1coghm  25220  caubl  25467  caublcls  25468  cniccbdd  25620  ovolfioo  25626  ovolficc  25627  ovolfsval  25629  ovolicc2lem1  25676  ovolicc2lem4  25679  ovolicc2lem5  25680  volsup  25715  uniiccdif  25737  uniioovol  25738  uniiccvol  25739  uniioombllem2  25742  uniioombllem3a  25743  uniioombllem4  25745  uniioombllem5  25746  mbfimaopnlem  25814  limccnp  26050  dvcobr  26105  dvcjbr  26108  dvfre  26110  plycjlem  26433  plycj  26434  coecj  26435  plycjOLD  26436  coecjOLD  26437  radcnvlem2  26577  radcnvlem3  26578  radcnvlt2  26582  pserulm  26585  resinf1o  26701  jensen  27153  eflgam  27209  ftalem3  27239  dchrinv  27425  dchr2sum  27437  dchrisum0re  27677  motco  28809  motcgrg  28813  ex-co  30789  vafval  30955  smfval  30957  vsfval  30985  imsdval  31038  lnocoi  31109  occllem  31655  hocoi  32116  homco1  32153  counop  32273  homco2  32329  hmopco  32375  nlelchi  32413  kbass2  32469  kbass5  32472  leopsq  32481  hmopidmchi  32503  elpjrn  32542  pjinvari  32543  cycpmco2  33453  derangenlem  35663  subfacp1lem5  35676  cnpconn  35722  txsconnlem  35732  txsconn  35733  cvmliftmolem1  35773  cvmliftlem7  35783  cvmlift2lem3  35797  cvmlift2lem7  35801  cvmlift2lem9  35803  cvmliftphtlem  35809  cvmlift3lem1  35811  cvmlift3lem2  35812  cvmlift3lem4  35814  cvmlift3lem5  35815  cvmlift3lem6  35816  cvmlift3lem7  35817  mrsubco  36013  msubco  36023  mclsppslem  36075  sinccvglem  36164  iprodefisumlem  36232  iprodefisum  36233  poimirlem22  38293  mblfinlem2  38309  ftc1anclem5  38348  ftc1anclem8  38351  cocanfo  38370  f1ocan1fv  38377  upixp  38380  ghomco  38542  rngohomco  38625  lautco  40871  ldilco  40890  ltrncoval  40919  tendocoval  41540  tendoconid  41603  tendospass  41793  dicvscacl  41965  cdlemn3  41971  cdlemn9  41979  brcoffn  44756  fvovco  45911  climexp  46321  stoweidlem27  46741  stoweidlem31  46745  ovolval4lem1  47363  gricushgr  48682  uspgrlimlem3  48755  uspgrlimlem4  48756  grlictr  48780