Theorem fvco3 6941

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ∘ ccom 5636   Fn wfn 6495  ⟶wf 6496  ‘cfv 6500

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 5243  ax-nul 5253  ax-pr 5379

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508

This theorem is referenced by:  fvco3d  6942  foco2  7063  f1cofveqaeqALT  7214  f1ocnvfv1  7232  f1ocnvfv2  7233  fcof1  7243  fcofo  7244  cocan1  7247  cocan2  7248  fveqf1o  7258  isotr  7292  fipreima  9270  fsuppco2  9318  fsuppcor  9319  unxpwdom2  9505  wemapwe  9618  ackbij2lem2  10161  cofsmo  10191  cfcoflem  10194  isf32lem6  10280  isf32lem7  10281  isf32lem8  10282  isf34lem7  10301  isf34lem6  10302  axcc3  10360  axdc4lem  10377  inar1  10698  axdc4uzlem  13918  seqf1olem2  13977  seqf1o  13978  lswco  14774  lo1o1  15467  o1co  15521  caucvgrlem2  15610  summolem3  15649  fsumf1o  15658  fsumcl2lem  15666  fsumadd  15675  fsummulc2  15719  fsumrelem  15742  supcvg  15791  prodmolem3  15868  fprodf1o  15881  fprodser  15884  fprodcl2lem  15885  fprodmul  15895  fproddiv  15896  fprodn0  15914  ruclem11  16177  ruclem12  16178  algcvg  16515  eulerthlem2  16721  cofu1  17820  cofu2  17822  cofucl  17824  fucidcl  17904  fuclid  17905  fucrid  17906  homadm  17976  homacd  17977  evlfcl  18157  curfuncf  18173  yonedalem4c  18212  yonedalem3b  18214  mgmhmco  18651  mhmco  18760  prdspjmhm  18766  pwsco1mhm  18769  lactghmga  19346  frgpup3lem  19718  gsumval3eu  19845  gsumval3  19848  gsumzaddlem  19862  gsumzmhm  19878  dprdf1o  19975  gsumfsum  21401  zrhpsgninv  21552  zrhpsgnevpm  21558  zrhpsgnodpm  21559  evlssca  22061  evls1val  22276  evls1sca  22279  evl1val  22285  mdetralt  22564  mdetunilem7  22574  cpmadumatpoly  22839  chcoeffeqlem  22841  cnpco  23223  lmcnp  23260  upxp  23579  uptx  23581  cnmpt11  23619  cnmpt21  23627  xkofvcn  23640  prdstmdd  24080  prdstgpd  24081  comet  24469  prdsxmslem2  24485  nrmmetd  24530  isngp3  24554  ngpds  24560  tngnm  24607  nmoco  24693  cnmetdval  24726  climcncf  24861  cncfco  24868  htpyco1  24945  htpyco2  24946  phtpyco2  24957  reparphti  24964  reparphtiOLD  24965  copco  24986  pi1cof  25027  pi1coghm  25029  caubl  25276  caublcls  25277  cniccbdd  25430  ovolfioo  25436  ovolficc  25437  ovolfsval  25439  ovolicc2lem1  25486  ovolicc2lem4  25489  ovolicc2lem5  25490  volsup  25525  uniiccdif  25547  uniioovol  25548  uniiccvol  25549  uniioombllem2  25552  uniioombllem3a  25553  uniioombllem4  25555  uniioombllem5  25556  mbfimaopnlem  25624  limccnp  25860  dvcobr  25917  dvcobrOLD  25918  dvcjbr  25921  dvfre  25923  plycjlem  26250  plycj  26251  coecj  26252  plycjOLD  26253  coecjOLD  26254  radcnvlem2  26391  radcnvlem3  26392  radcnvlt2  26396  pserulm  26399  resinf1o  26513  jensen  26967  eflgam  27023  ftalem3  27053  dchrinv  27240  dchr2sum  27252  dchrisum0re  27492  motco  28624  motcgrg  28628  ex-co  30525  vafval  30691  smfval  30693  vsfval  30721  imsdval  30774  lnocoi  30845  occllem  31391  hocoi  31852  homco1  31889  counop  32009  homco2  32065  hmopco  32111  nlelchi  32149  kbass2  32205  kbass5  32208  leopsq  32217  hmopidmchi  32239  elpjrn  32278  pjinvari  32279  cycpmco2  33227  derangenlem  35387  subfacp1lem5  35400  cnpconn  35446  txsconnlem  35456  txsconn  35457  cvmliftmolem1  35497  cvmliftlem7  35507  cvmlift2lem3  35521  cvmlift2lem7  35525  cvmlift2lem9  35527  cvmliftphtlem  35533  cvmlift3lem1  35535  cvmlift3lem2  35536  cvmlift3lem4  35538  cvmlift3lem5  35539  cvmlift3lem6  35540  cvmlift3lem7  35541  mrsubco  35737  msubco  35747  mclsppslem  35799  sinccvglem  35888  iprodefisumlem  35956  iprodefisum  35957  poimirlem22  37893  mblfinlem2  37909  ftc1anclem5  37948  ftc1anclem8  37951  cocanfo  37970  f1ocan1fv  37977  upixp  37980  ghomco  38142  rngohomco  38225  lautco  40473  ldilco  40492  ltrncoval  40521  tendocoval  41142  tendoconid  41205  tendospass  41395  dicvscacl  41567  cdlemn3  41573  cdlemn9  41581  brcoffn  44386  fvovco  45552  climexp  45965  stoweidlem27  46385  stoweidlem31  46389  ovolval4lem1  47007  gricushgr  48277  uspgrlimlem3  48350  uspgrlimlem4  48351  grlictr  48375