Theorem fvco3 6991

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1539   ∈ wcel 2104   ∘ ccom 5681   Fn wfn 6539  ⟶wf 6540  ‘cfv 6544

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552

This theorem is referenced by:  fvco3d  6992  foco2  7111  f1cofveqaeqALT  7262  f1ocnvfv1  7278  f1ocnvfv2  7279  fcof1  7289  fcofo  7290  cocan1  7293  cocan2  7294  fveqf1o  7305  isotr  7337  fipreima  9362  fsuppco2  9402  fsuppcor  9403  unxpwdom2  9587  wemapwe  9696  ackbij2lem2  10239  cofsmo  10268  cfcoflem  10271  isf32lem6  10357  isf32lem7  10358  isf32lem8  10359  isf34lem7  10378  isf34lem6  10379  axcc3  10437  axdc4lem  10454  inar1  10774  axdc4uzlem  13954  seqf1olem2  14014  seqf1o  14015  lswco  14796  lo1o1  15482  o1co  15536  caucvgrlem2  15627  summolem3  15666  fsumf1o  15675  fsumcl2lem  15683  fsumadd  15692  fsummulc2  15736  fsumrelem  15759  supcvg  15808  prodmolem3  15883  fprodf1o  15896  fprodser  15899  fprodcl2lem  15900  fprodmul  15910  fproddiv  15911  fprodn0  15929  ruclem11  16189  ruclem12  16190  algcvg  16519  eulerthlem2  16721  cofu1  17840  cofu2  17842  cofucl  17844  fucidcl  17924  fuclid  17925  fucrid  17926  homadm  17996  homacd  17997  evlfcl  18181  curfuncf  18197  yonedalem4c  18236  yonedalem3b  18238  mgmhmco  18641  mhmco  18742  prdspjmhm  18748  pwsco1mhm  18751  lactghmga  19316  frgpup3lem  19688  gsumval3eu  19815  gsumval3  19818  gsumzaddlem  19832  gsumzmhm  19848  dprdf1o  19945  gsumfsum  21214  zrhpsgninv  21359  zrhpsgnevpm  21365  zrhpsgnodpm  21366  evlssca  21873  evls1val  22061  evls1sca  22064  evl1val  22070  mdetralt  22332  mdetunilem7  22342  cpmadumatpoly  22607  chcoeffeqlem  22609  cnpco  22993  lmcnp  23030  upxp  23349  uptx  23351  cnmpt11  23389  cnmpt21  23397  xkofvcn  23410  prdstmdd  23850  prdstgpd  23851  comet  24244  prdsxmslem2  24260  nrmmetd  24305  isngp3  24329  ngpds  24335  tngnm  24390  nmoco  24476  cnmetdval  24509  climcncf  24642  cncfco  24649  htpyco1  24726  htpyco2  24727  phtpyco2  24738  reparphti  24745  reparphtiOLD  24746  copco  24767  pi1cof  24808  pi1coghm  24810  caubl  25058  caublcls  25059  cniccbdd  25212  ovolfioo  25218  ovolficc  25219  ovolfsval  25221  ovolicc2lem1  25268  ovolicc2lem4  25271  ovolicc2lem5  25272  volsup  25307  uniiccdif  25329  uniioovol  25330  uniiccvol  25331  uniioombllem2  25334  uniioombllem3a  25335  uniioombllem4  25337  uniioombllem5  25338  mbfimaopnlem  25406  limccnp  25642  dvcobr  25697  dvcjbr  25700  dvfre  25702  plycjlem  26024  plycj  26025  coecj  26026  radcnvlem2  26160  radcnvlem3  26161  radcnvlt2  26165  pserulm  26168  resinf1o  26279  jensen  26727  eflgam  26783  ftalem3  26813  dchrinv  26998  dchr2sum  27010  dchrisum0re  27250  motco  28056  motcgrg  28060  ex-co  29956  vafval  30121  smfval  30123  vsfval  30151  imsdval  30204  lnocoi  30275  occllem  30821  hocoi  31282  homco1  31319  counop  31439  homco2  31495  hmopco  31541  nlelchi  31579  kbass2  31635  kbass5  31638  leopsq  31647  hmopidmchi  31669  elpjrn  31708  pjinvari  31709  cycpmco2  32560  derangenlem  34458  subfacp1lem5  34471  cnpconn  34517  txsconnlem  34527  txsconn  34528  cvmliftmolem1  34568  cvmliftlem7  34578  cvmlift2lem3  34592  cvmlift2lem7  34596  cvmlift2lem9  34598  cvmliftphtlem  34604  cvmlift3lem1  34606  cvmlift3lem2  34607  cvmlift3lem4  34609  cvmlift3lem5  34610  cvmlift3lem6  34611  cvmlift3lem7  34612  mrsubco  34808  msubco  34818  mclsppslem  34870  sinccvglem  34953  iprodefisumlem  35012  iprodefisum  35013  gg-dvcobr  35464  poimirlem22  36815  mblfinlem2  36831  ftc1anclem5  36870  ftc1anclem8  36873  cocanfo  36892  f1ocan1fv  36899  upixp  36902  ghomco  37064  rngohomco  37147  lautco  39273  ldilco  39292  ltrncoval  39321  tendocoval  39942  tendoconid  40005  tendospass  40195  dicvscacl  40367  cdlemn3  40373  cdlemn9  40381  brcoffn  43085  fvovco  44192  climexp  44621  stoweidlem27  45043  stoweidlem31  45047  ovolval4lem1  45665  isomushgr  46794