Theorem fvco3 6978

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108   ∘ ccom 5658   Fn wfn 6526  ⟶wf 6527  ‘cfv 6531

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539

This theorem is referenced by:  fvco3d  6979  foco2  7099  f1cofveqaeqALT  7251  f1ocnvfv1  7269  f1ocnvfv2  7270  fcof1  7280  fcofo  7281  cocan1  7284  cocan2  7285  fveqf1o  7295  isotr  7329  fipreima  9370  fsuppco2  9415  fsuppcor  9416  unxpwdom2  9602  wemapwe  9711  ackbij2lem2  10253  cofsmo  10283  cfcoflem  10286  isf32lem6  10372  isf32lem7  10373  isf32lem8  10374  isf34lem7  10393  isf34lem6  10394  axcc3  10452  axdc4lem  10469  inar1  10789  axdc4uzlem  14001  seqf1olem2  14060  seqf1o  14061  lswco  14858  lo1o1  15548  o1co  15602  caucvgrlem2  15691  summolem3  15730  fsumf1o  15739  fsumcl2lem  15747  fsumadd  15756  fsummulc2  15800  fsumrelem  15823  supcvg  15872  prodmolem3  15949  fprodf1o  15962  fprodser  15965  fprodcl2lem  15966  fprodmul  15976  fproddiv  15977  fprodn0  15995  ruclem11  16258  ruclem12  16259  algcvg  16595  eulerthlem2  16801  cofu1  17897  cofu2  17899  cofucl  17901  fucidcl  17981  fuclid  17982  fucrid  17983  homadm  18053  homacd  18054  evlfcl  18234  curfuncf  18250  yonedalem4c  18289  yonedalem3b  18291  mgmhmco  18692  mhmco  18801  prdspjmhm  18807  pwsco1mhm  18810  lactghmga  19386  frgpup3lem  19758  gsumval3eu  19885  gsumval3  19888  gsumzaddlem  19902  gsumzmhm  19918  dprdf1o  20015  gsumfsum  21402  zrhpsgninv  21545  zrhpsgnevpm  21551  zrhpsgnodpm  21552  evlssca  22047  evls1val  22258  evls1sca  22261  evl1val  22267  mdetralt  22546  mdetunilem7  22556  cpmadumatpoly  22821  chcoeffeqlem  22823  cnpco  23205  lmcnp  23242  upxp  23561  uptx  23563  cnmpt11  23601  cnmpt21  23609  xkofvcn  23622  prdstmdd  24062  prdstgpd  24063  comet  24452  prdsxmslem2  24468  nrmmetd  24513  isngp3  24537  ngpds  24543  tngnm  24590  nmoco  24676  cnmetdval  24709  climcncf  24844  cncfco  24851  htpyco1  24928  htpyco2  24929  phtpyco2  24940  reparphti  24947  reparphtiOLD  24948  copco  24969  pi1cof  25010  pi1coghm  25012  caubl  25260  caublcls  25261  cniccbdd  25414  ovolfioo  25420  ovolficc  25421  ovolfsval  25423  ovolicc2lem1  25470  ovolicc2lem4  25473  ovolicc2lem5  25474  volsup  25509  uniiccdif  25531  uniioovol  25532  uniiccvol  25533  uniioombllem2  25536  uniioombllem3a  25537  uniioombllem4  25539  uniioombllem5  25540  mbfimaopnlem  25608  limccnp  25844  dvcobr  25901  dvcobrOLD  25902  dvcjbr  25905  dvfre  25907  plycjlem  26234  plycj  26235  coecj  26236  plycjOLD  26237  coecjOLD  26238  radcnvlem2  26375  radcnvlem3  26376  radcnvlt2  26380  pserulm  26383  resinf1o  26497  jensen  26951  eflgam  27007  ftalem3  27037  dchrinv  27224  dchr2sum  27236  dchrisum0re  27476  motco  28519  motcgrg  28523  ex-co  30419  vafval  30584  smfval  30586  vsfval  30614  imsdval  30667  lnocoi  30738  occllem  31284  hocoi  31745  homco1  31782  counop  31902  homco2  31958  hmopco  32004  nlelchi  32042  kbass2  32098  kbass5  32101  leopsq  32110  hmopidmchi  32132  elpjrn  32171  pjinvari  32172  cycpmco2  33144  derangenlem  35193  subfacp1lem5  35206  cnpconn  35252  txsconnlem  35262  txsconn  35263  cvmliftmolem1  35303  cvmliftlem7  35313  cvmlift2lem3  35327  cvmlift2lem7  35331  cvmlift2lem9  35333  cvmliftphtlem  35339  cvmlift3lem1  35341  cvmlift3lem2  35342  cvmlift3lem4  35344  cvmlift3lem5  35345  cvmlift3lem6  35346  cvmlift3lem7  35347  mrsubco  35543  msubco  35553  mclsppslem  35605  sinccvglem  35694  iprodefisumlem  35757  iprodefisum  35758  poimirlem22  37666  mblfinlem2  37682  ftc1anclem5  37721  ftc1anclem8  37724  cocanfo  37743  f1ocan1fv  37750  upixp  37753  ghomco  37915  rngohomco  37998  lautco  40116  ldilco  40135  ltrncoval  40164  tendocoval  40785  tendoconid  40848  tendospass  41038  dicvscacl  41210  cdlemn3  41216  cdlemn9  41224  brcoffn  44054  fvovco  45217  climexp  45634  stoweidlem27  46056  stoweidlem31  46060  ovolval4lem1  46678  gricushgr  47930  uspgrlimlem3  48002  uspgrlimlem4  48003  grlictr  48020