Theorem fvco3 6967

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560   ∈ wcel 2142   ∘ ccom 5651   Fn wfn 6516  ⟶wf 6517  ‘cfv 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-fv 6529

This theorem is referenced by:  fvco3d  6968  foco2  7090  f1cofveqaeqALT  7242  f1ocnvfv1  7260  f1ocnvfv2  7261  fcof1  7271  fcofo  7272  cocan1  7275  cocan2  7276  fveqf1o  7286  isotr  7320  fipreima  9301  fsuppco2  9349  fsuppcor  9350  unxpwdom2  9536  wemapwe  9652  ackbij2lem2  10195  cofsmo  10226  cfcoflem  10229  isf32lem6  10315  isf32lem7  10316  isf32lem8  10317  isf34lem7  10336  isf34lem6  10337  axcc3  10395  axdc4lem  10412  inar1  10733  axdc4uzlem  13996  seqf1olem2  14055  seqf1o  14056  lswco  14852  lo1o1  15559  o1co  15613  caucvgrlem2  15702  summolem3  15741  fsumf1o  15750  fsumcl2lem  15758  fsumadd  15767  fsummulc2  15811  fsumrelem  15835  supcvg  15886  prodmolem3  15963  fprodf1o  15976  fprodser  15979  fprodcl2lem  15980  fprodmul  15990  fproddiv  15991  fprodn0  16009  ruclem11  16272  ruclem12  16273  algcvg  16610  eulerthlem2  16817  cofu1  17917  cofu2  17919  cofucl  17921  fucidcl  18001  fuclid  18002  fucrid  18003  homadm  18073  homacd  18074  evlfcl  18254  curfuncf  18270  yonedalem4c  18309  yonedalem3b  18311  mgmhmco  18748  mhmco  18857  prdspjmhm  18863  pwsco1mhm  18866  lactghmga  19445  frgpup3lem  19817  gsumval3eu  19944  gsumval3  19947  gsumzaddlem  19961  gsumzmhm  19977  dprdf1o  20074  gsumfsum  21486  zrhpsgninv  21637  zrhpsgnevpm  21643  zrhpsgnodpm  21644  evlssca  22147  evls1val  22383  evls1sca  22386  evl1val  22392  mdetralt  22668  mdetunilem7  22678  cpmadumatpoly  22943  chcoeffeqlem  22945  cnpco  23327  lmcnp  23364  upxp  23683  uptx  23685  cnmpt11  23723  cnmpt21  23731  xkofvcn  23744  prdstmdd  24184  prdstgpd  24185  comet  24573  prdsxmslem2  24589  nrmmetd  24634  isngp3  24658  ngpds  24664  tngnm  24711  nmoco  24797  cnmetdval  24830  climcncf  24962  cncfco  24969  htpyco1  25040  htpyco2  25041  phtpyco2  25052  reparphti  25059  copco  25080  pi1cof  25121  pi1coghm  25123  caubl  25370  caublcls  25371  cniccbdd  25523  ovolfioo  25529  ovolficc  25530  ovolfsval  25532  ovolicc2lem1  25579  ovolicc2lem4  25582  ovolicc2lem5  25583  volsup  25618  uniiccdif  25640  uniioovol  25641  uniiccvol  25642  uniioombllem2  25645  uniioombllem3a  25646  uniioombllem4  25648  uniioombllem5  25649  mbfimaopnlem  25717  limccnp  25953  dvcobr  26008  dvcjbr  26011  dvfre  26013  plycjlem  26336  plycj  26337  coecj  26338  plycjOLD  26339  coecjOLD  26340  radcnvlem2  26477  radcnvlem3  26478  radcnvlt2  26482  pserulm  26485  resinf1o  26601  jensen  27053  eflgam  27109  ftalem3  27139  dchrinv  27325  dchr2sum  27337  dchrisum0re  27577  motco  28709  motcgrg  28713  ex-co  30640  vafval  30806  smfval  30808  vsfval  30836  imsdval  30889  lnocoi  30960  occllem  31506  hocoi  31967  homco1  32004  counop  32124  homco2  32180  hmopco  32226  nlelchi  32264  kbass2  32320  kbass5  32323  leopsq  32332  hmopidmchi  32354  elpjrn  32393  pjinvari  32394  cycpmco2  33313  derangenlem  35521  subfacp1lem5  35534  cnpconn  35580  txsconnlem  35590  txsconn  35591  cvmliftmolem1  35631  cvmliftlem7  35641  cvmlift2lem3  35655  cvmlift2lem7  35659  cvmlift2lem9  35661  cvmliftphtlem  35667  cvmlift3lem1  35669  cvmlift3lem2  35670  cvmlift3lem4  35672  cvmlift3lem5  35673  cvmlift3lem6  35674  cvmlift3lem7  35675  mrsubco  35871  msubco  35881  mclsppslem  35933  sinccvglem  36022  iprodefisumlem  36090  iprodefisum  36091  poimirlem22  38141  mblfinlem2  38157  ftc1anclem5  38196  ftc1anclem8  38199  cocanfo  38218  f1ocan1fv  38225  upixp  38228  ghomco  38390  rngohomco  38473  lautco  40721  ldilco  40740  ltrncoval  40769  tendocoval  41390  tendoconid  41453  tendospass  41643  dicvscacl  41815  cdlemn3  41821  cdlemn9  41829  brcoffn  44606  fvovco  45771  climexp  46181  stoweidlem27  46601  stoweidlem31  46605  ovolval4lem1  47223  gricushgr  48539  uspgrlimlem3  48612  uspgrlimlem4  48613  grlictr  48637