Theorem fvco3 6939

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ∘ ccom 5635   Fn wfn 6493  ⟶wf 6494  ‘cfv 6498

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 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-fv 6506

This theorem is referenced by:  fvco3d  6940  foco2  7061  f1cofveqaeqALT  7213  f1ocnvfv1  7231  f1ocnvfv2  7232  fcof1  7242  fcofo  7243  cocan1  7246  cocan2  7247  fveqf1o  7257  isotr  7291  fipreima  9268  fsuppco2  9316  fsuppcor  9317  unxpwdom2  9503  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  13945  seqf1olem2  14004  seqf1o  14005  lswco  14801  lo1o1  15494  o1co  15548  caucvgrlem2  15637  summolem3  15676  fsumf1o  15685  fsumcl2lem  15693  fsumadd  15702  fsummulc2  15746  fsumrelem  15770  supcvg  15821  prodmolem3  15898  fprodf1o  15911  fprodser  15914  fprodcl2lem  15915  fprodmul  15925  fproddiv  15926  fprodn0  15944  ruclem11  16207  ruclem12  16208  algcvg  16545  eulerthlem2  16752  cofu1  17851  cofu2  17853  cofucl  17855  fucidcl  17935  fuclid  17936  fucrid  17937  homadm  18007  homacd  18008  evlfcl  18188  curfuncf  18204  yonedalem4c  18243  yonedalem3b  18245  mgmhmco  18682  mhmco  18791  prdspjmhm  18797  pwsco1mhm  18800  lactghmga  19380  frgpup3lem  19752  gsumval3eu  19879  gsumval3  19882  gsumzaddlem  19896  gsumzmhm  19912  dprdf1o  20009  gsumfsum  21414  zrhpsgninv  21565  zrhpsgnevpm  21571  zrhpsgnodpm  21572  evlssca  22072  evls1val  22285  evls1sca  22288  evl1val  22294  mdetralt  22573  mdetunilem7  22583  cpmadumatpoly  22848  chcoeffeqlem  22850  cnpco  23232  lmcnp  23269  upxp  23588  uptx  23590  cnmpt11  23628  cnmpt21  23636  xkofvcn  23649  prdstmdd  24089  prdstgpd  24090  comet  24478  prdsxmslem2  24494  nrmmetd  24539  isngp3  24563  ngpds  24569  tngnm  24616  nmoco  24702  cnmetdval  24735  climcncf  24867  cncfco  24874  htpyco1  24945  htpyco2  24946  phtpyco2  24957  reparphti  24964  copco  24985  pi1cof  25026  pi1coghm  25028  caubl  25275  caublcls  25276  cniccbdd  25428  ovolfioo  25434  ovolficc  25435  ovolfsval  25437  ovolicc2lem1  25484  ovolicc2lem4  25487  ovolicc2lem5  25488  volsup  25523  uniiccdif  25545  uniioovol  25546  uniiccvol  25547  uniioombllem2  25550  uniioombllem3a  25551  uniioombllem4  25553  uniioombllem5  25554  mbfimaopnlem  25622  limccnp  25858  dvcobr  25913  dvcjbr  25916  dvfre  25918  plycjlem  26241  plycj  26242  coecj  26243  plycjOLD  26244  coecjOLD  26245  radcnvlem2  26379  radcnvlem3  26380  radcnvlt2  26384  pserulm  26387  resinf1o  26500  jensen  26952  eflgam  27008  ftalem3  27038  dchrinv  27224  dchr2sum  27236  dchrisum0re  27476  motco  28608  motcgrg  28612  ex-co  30508  vafval  30674  smfval  30676  vsfval  30704  imsdval  30757  lnocoi  30828  occllem  31374  hocoi  31835  homco1  31872  counop  31992  homco2  32048  hmopco  32094  nlelchi  32132  kbass2  32188  kbass5  32191  leopsq  32200  hmopidmchi  32222  elpjrn  32261  pjinvari  32262  cycpmco2  33194  derangenlem  35353  subfacp1lem5  35366  cnpconn  35412  txsconnlem  35422  txsconn  35423  cvmliftmolem1  35463  cvmliftlem7  35473  cvmlift2lem3  35487  cvmlift2lem7  35491  cvmlift2lem9  35493  cvmliftphtlem  35499  cvmlift3lem1  35501  cvmlift3lem2  35502  cvmlift3lem4  35504  cvmlift3lem5  35505  cvmlift3lem6  35506  cvmlift3lem7  35507  mrsubco  35703  msubco  35713  mclsppslem  35765  sinccvglem  35854  iprodefisumlem  35922  iprodefisum  35923  poimirlem22  37963  mblfinlem2  37979  ftc1anclem5  38018  ftc1anclem8  38021  cocanfo  38040  f1ocan1fv  38047  upixp  38050  ghomco  38212  rngohomco  38295  lautco  40543  ldilco  40562  ltrncoval  40591  tendocoval  41212  tendoconid  41275  tendospass  41465  dicvscacl  41637  cdlemn3  41643  cdlemn9  41651  brcoffn  44457  fvovco  45623  climexp  46035  stoweidlem27  46455  stoweidlem31  46459  ovolval4lem1  47077  gricushgr  48393  uspgrlimlem3  48466  uspgrlimlem4  48467  grlictr  48491