Theorem fvco3 7008

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108   ∘ ccom 5689   Fn wfn 6556  ⟶wf 6557  ‘cfv 6561

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 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569

This theorem is referenced by:  fvco3d  7009  foco2  7129  f1cofveqaeqALT  7279  f1ocnvfv1  7296  f1ocnvfv2  7297  fcof1  7307  fcofo  7308  cocan1  7311  cocan2  7312  fveqf1o  7322  isotr  7356  fipreima  9398  fsuppco2  9443  fsuppcor  9444  unxpwdom2  9628  wemapwe  9737  ackbij2lem2  10279  cofsmo  10309  cfcoflem  10312  isf32lem6  10398  isf32lem7  10399  isf32lem8  10400  isf34lem7  10419  isf34lem6  10420  axcc3  10478  axdc4lem  10495  inar1  10815  axdc4uzlem  14024  seqf1olem2  14083  seqf1o  14084  lswco  14878  lo1o1  15568  o1co  15622  caucvgrlem2  15711  summolem3  15750  fsumf1o  15759  fsumcl2lem  15767  fsumadd  15776  fsummulc2  15820  fsumrelem  15843  supcvg  15892  prodmolem3  15969  fprodf1o  15982  fprodser  15985  fprodcl2lem  15986  fprodmul  15996  fproddiv  15997  fprodn0  16015  ruclem11  16276  ruclem12  16277  algcvg  16613  eulerthlem2  16819  cofu1  17929  cofu2  17931  cofucl  17933  fucidcl  18013  fuclid  18014  fucrid  18015  homadm  18085  homacd  18086  evlfcl  18267  curfuncf  18283  yonedalem4c  18322  yonedalem3b  18324  mgmhmco  18727  mhmco  18836  prdspjmhm  18842  pwsco1mhm  18845  lactghmga  19423  frgpup3lem  19795  gsumval3eu  19922  gsumval3  19925  gsumzaddlem  19939  gsumzmhm  19955  dprdf1o  20052  gsumfsum  21452  zrhpsgninv  21603  zrhpsgnevpm  21609  zrhpsgnodpm  21610  evlssca  22113  evls1val  22324  evls1sca  22327  evl1val  22333  mdetralt  22614  mdetunilem7  22624  cpmadumatpoly  22889  chcoeffeqlem  22891  cnpco  23275  lmcnp  23312  upxp  23631  uptx  23633  cnmpt11  23671  cnmpt21  23679  xkofvcn  23692  prdstmdd  24132  prdstgpd  24133  comet  24526  prdsxmslem2  24542  nrmmetd  24587  isngp3  24611  ngpds  24617  tngnm  24672  nmoco  24758  cnmetdval  24791  climcncf  24926  cncfco  24933  htpyco1  25010  htpyco2  25011  phtpyco2  25022  reparphti  25029  reparphtiOLD  25030  copco  25051  pi1cof  25092  pi1coghm  25094  caubl  25342  caublcls  25343  cniccbdd  25496  ovolfioo  25502  ovolficc  25503  ovolfsval  25505  ovolicc2lem1  25552  ovolicc2lem4  25555  ovolicc2lem5  25556  volsup  25591  uniiccdif  25613  uniioovol  25614  uniiccvol  25615  uniioombllem2  25618  uniioombllem3a  25619  uniioombllem4  25621  uniioombllem5  25622  mbfimaopnlem  25690  limccnp  25926  dvcobr  25983  dvcobrOLD  25984  dvcjbr  25987  dvfre  25989  plycjlem  26316  plycj  26317  coecj  26318  plycjOLD  26319  coecjOLD  26320  radcnvlem2  26457  radcnvlem3  26458  radcnvlt2  26462  pserulm  26465  resinf1o  26578  jensen  27032  eflgam  27088  ftalem3  27118  dchrinv  27305  dchr2sum  27317  dchrisum0re  27557  motco  28548  motcgrg  28552  ex-co  30457  vafval  30622  smfval  30624  vsfval  30652  imsdval  30705  lnocoi  30776  occllem  31322  hocoi  31783  homco1  31820  counop  31940  homco2  31996  hmopco  32042  nlelchi  32080  kbass2  32136  kbass5  32139  leopsq  32148  hmopidmchi  32170  elpjrn  32209  pjinvari  32210  cycpmco2  33153  derangenlem  35176  subfacp1lem5  35189  cnpconn  35235  txsconnlem  35245  txsconn  35246  cvmliftmolem1  35286  cvmliftlem7  35296  cvmlift2lem3  35310  cvmlift2lem7  35314  cvmlift2lem9  35316  cvmliftphtlem  35322  cvmlift3lem1  35324  cvmlift3lem2  35325  cvmlift3lem4  35327  cvmlift3lem5  35328  cvmlift3lem6  35329  cvmlift3lem7  35330  mrsubco  35526  msubco  35536  mclsppslem  35588  sinccvglem  35677  iprodefisumlem  35740  iprodefisum  35741  poimirlem22  37649  mblfinlem2  37665  ftc1anclem5  37704  ftc1anclem8  37707  cocanfo  37726  f1ocan1fv  37733  upixp  37736  ghomco  37898  rngohomco  37981  lautco  40099  ldilco  40118  ltrncoval  40147  tendocoval  40768  tendoconid  40831  tendospass  41021  dicvscacl  41193  cdlemn3  41199  cdlemn9  41207  brcoffn  44043  fvovco  45198  climexp  45620  stoweidlem27  46042  stoweidlem31  46046  ovolval4lem1  46664  gricushgr  47886  uspgrlimlem3  47957  uspgrlimlem4  47958  grlictr  47975