Theorem fvco3 6963

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ∘ ccom 5645   Fn wfn 6509  ⟶wf 6510  ‘cfv 6514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-fv 6522

This theorem is referenced by:  fvco3d  6964  foco2  7084  f1cofveqaeqALT  7236  f1ocnvfv1  7254  f1ocnvfv2  7255  fcof1  7265  fcofo  7266  cocan1  7269  cocan2  7270  fveqf1o  7280  isotr  7314  fipreima  9316  fsuppco2  9361  fsuppcor  9362  unxpwdom2  9548  wemapwe  9657  ackbij2lem2  10199  cofsmo  10229  cfcoflem  10232  isf32lem6  10318  isf32lem7  10319  isf32lem8  10320  isf34lem7  10339  isf34lem6  10340  axcc3  10398  axdc4lem  10415  inar1  10735  axdc4uzlem  13955  seqf1olem2  14014  seqf1o  14015  lswco  14812  lo1o1  15505  o1co  15559  caucvgrlem2  15648  summolem3  15687  fsumf1o  15696  fsumcl2lem  15704  fsumadd  15713  fsummulc2  15757  fsumrelem  15780  supcvg  15829  prodmolem3  15906  fprodf1o  15919  fprodser  15922  fprodcl2lem  15923  fprodmul  15933  fproddiv  15934  fprodn0  15952  ruclem11  16215  ruclem12  16216  algcvg  16553  eulerthlem2  16759  cofu1  17853  cofu2  17855  cofucl  17857  fucidcl  17937  fuclid  17938  fucrid  17939  homadm  18009  homacd  18010  evlfcl  18190  curfuncf  18206  yonedalem4c  18245  yonedalem3b  18247  mgmhmco  18648  mhmco  18757  prdspjmhm  18763  pwsco1mhm  18766  lactghmga  19342  frgpup3lem  19714  gsumval3eu  19841  gsumval3  19844  gsumzaddlem  19858  gsumzmhm  19874  dprdf1o  19971  gsumfsum  21358  zrhpsgninv  21501  zrhpsgnevpm  21507  zrhpsgnodpm  21508  evlssca  22003  evls1val  22214  evls1sca  22217  evl1val  22223  mdetralt  22502  mdetunilem7  22512  cpmadumatpoly  22777  chcoeffeqlem  22779  cnpco  23161  lmcnp  23198  upxp  23517  uptx  23519  cnmpt11  23557  cnmpt21  23565  xkofvcn  23578  prdstmdd  24018  prdstgpd  24019  comet  24408  prdsxmslem2  24424  nrmmetd  24469  isngp3  24493  ngpds  24499  tngnm  24546  nmoco  24632  cnmetdval  24665  climcncf  24800  cncfco  24807  htpyco1  24884  htpyco2  24885  phtpyco2  24896  reparphti  24903  reparphtiOLD  24904  copco  24925  pi1cof  24966  pi1coghm  24968  caubl  25215  caublcls  25216  cniccbdd  25369  ovolfioo  25375  ovolficc  25376  ovolfsval  25378  ovolicc2lem1  25425  ovolicc2lem4  25428  ovolicc2lem5  25429  volsup  25464  uniiccdif  25486  uniioovol  25487  uniiccvol  25488  uniioombllem2  25491  uniioombllem3a  25492  uniioombllem4  25494  uniioombllem5  25495  mbfimaopnlem  25563  limccnp  25799  dvcobr  25856  dvcobrOLD  25857  dvcjbr  25860  dvfre  25862  plycjlem  26189  plycj  26190  coecj  26191  plycjOLD  26192  coecjOLD  26193  radcnvlem2  26330  radcnvlem3  26331  radcnvlt2  26335  pserulm  26338  resinf1o  26452  jensen  26906  eflgam  26962  ftalem3  26992  dchrinv  27179  dchr2sum  27191  dchrisum0re  27431  motco  28474  motcgrg  28478  ex-co  30374  vafval  30539  smfval  30541  vsfval  30569  imsdval  30622  lnocoi  30693  occllem  31239  hocoi  31700  homco1  31737  counop  31857  homco2  31913  hmopco  31959  nlelchi  31997  kbass2  32053  kbass5  32056  leopsq  32065  hmopidmchi  32087  elpjrn  32126  pjinvari  32127  cycpmco2  33097  derangenlem  35165  subfacp1lem5  35178  cnpconn  35224  txsconnlem  35234  txsconn  35235  cvmliftmolem1  35275  cvmliftlem7  35285  cvmlift2lem3  35299  cvmlift2lem7  35303  cvmlift2lem9  35305  cvmliftphtlem  35311  cvmlift3lem1  35313  cvmlift3lem2  35314  cvmlift3lem4  35316  cvmlift3lem5  35317  cvmlift3lem6  35318  cvmlift3lem7  35319  mrsubco  35515  msubco  35525  mclsppslem  35577  sinccvglem  35666  iprodefisumlem  35734  iprodefisum  35735  poimirlem22  37643  mblfinlem2  37659  ftc1anclem5  37698  ftc1anclem8  37701  cocanfo  37720  f1ocan1fv  37727  upixp  37730  ghomco  37892  rngohomco  37975  lautco  40098  ldilco  40117  ltrncoval  40146  tendocoval  40767  tendoconid  40830  tendospass  41020  dicvscacl  41192  cdlemn3  41198  cdlemn9  41206  brcoffn  44026  fvovco  45194  climexp  45610  stoweidlem27  46032  stoweidlem31  46036  ovolval4lem1  46654  gricushgr  47921  uspgrlimlem3  47993  uspgrlimlem4  47994  grlictr  48011