Theorem fvco3 6867

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2106   ∘ ccom 5593   Fn wfn 6428  ⟶wf 6429  ‘cfv 6433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-fv 6441

This theorem is referenced by:  fvco3d  6868  foco2  6983  f1cofveqaeqALT  7132  f1ocnvfv1  7148  f1ocnvfv2  7149  fcof1  7159  fcofo  7160  cocan1  7163  cocan2  7164  fveqf1o  7175  isotr  7207  fipreima  9125  fsuppco2  9162  fsuppcor  9163  unxpwdom2  9347  wemapwe  9455  ackbij2lem2  9996  cofsmo  10025  cfcoflem  10028  isf32lem6  10114  isf32lem7  10115  isf32lem8  10116  isf34lem7  10135  isf34lem6  10136  axcc3  10194  axdc4lem  10211  inar1  10531  axdc4uzlem  13703  seqf1olem2  13763  seqf1o  13764  lswco  14552  lo1o1  15241  o1co  15295  caucvgrlem2  15386  summolem3  15426  fsumf1o  15435  fsumcl2lem  15443  fsumadd  15452  fsummulc2  15496  fsumrelem  15519  supcvg  15568  prodmolem3  15643  fprodf1o  15656  fprodser  15659  fprodcl2lem  15660  fprodmul  15670  fproddiv  15671  fprodn0  15689  ruclem11  15949  ruclem12  15950  algcvg  16281  eulerthlem2  16483  cofu1  17599  cofu2  17601  cofucl  17603  fucidcl  17683  fuclid  17684  fucrid  17685  homadm  17755  homacd  17756  evlfcl  17940  curfuncf  17956  yonedalem4c  17995  yonedalem3b  17997  mhmco  18462  prdspjmhm  18467  pwsco1mhm  18470  lactghmga  19013  frgpup3lem  19383  gsumval3eu  19505  gsumval3  19508  gsumzaddlem  19522  gsumzmhm  19538  dprdf1o  19635  gsumfsum  20665  zrhpsgninv  20790  zrhpsgnevpm  20796  zrhpsgnodpm  20797  evlssca  21299  evls1val  21486  evls1sca  21489  evl1val  21495  mdetralt  21757  mdetunilem7  21767  cpmadumatpoly  22032  chcoeffeqlem  22034  cnpco  22418  lmcnp  22455  upxp  22774  uptx  22776  cnmpt11  22814  cnmpt21  22822  xkofvcn  22835  prdstmdd  23275  prdstgpd  23276  comet  23669  prdsxmslem2  23685  nrmmetd  23730  isngp3  23754  ngpds  23760  tngnm  23815  nmoco  23901  cnmetdval  23934  climcncf  24063  cncfco  24070  htpyco1  24141  htpyco2  24142  phtpyco2  24153  reparphti  24160  copco  24181  pi1cof  24222  pi1coghm  24224  caubl  24472  caublcls  24473  cniccbdd  24625  ovolfioo  24631  ovolficc  24632  ovolfsval  24634  ovolicc2lem1  24681  ovolicc2lem4  24684  ovolicc2lem5  24685  volsup  24720  uniiccdif  24742  uniioovol  24743  uniiccvol  24744  uniioombllem2  24747  uniioombllem3a  24748  uniioombllem4  24750  uniioombllem5  24751  mbfimaopnlem  24819  limccnp  25055  dvcobr  25110  dvcjbr  25113  dvfre  25115  plycjlem  25437  plycj  25438  coecj  25439  radcnvlem2  25573  radcnvlem3  25574  radcnvlt2  25578  pserulm  25581  resinf1o  25692  jensen  26138  eflgam  26194  ftalem3  26224  dchrinv  26409  dchr2sum  26421  dchrisum0re  26661  motco  26901  motcgrg  26905  ex-co  28802  vafval  28965  smfval  28967  vsfval  28995  imsdval  29048  lnocoi  29119  occllem  29665  hocoi  30126  homco1  30163  counop  30283  homco2  30339  hmopco  30385  nlelchi  30423  kbass2  30479  kbass5  30482  leopsq  30491  hmopidmchi  30513  elpjrn  30552  pjinvari  30553  cycpmco2  31400  derangenlem  33133  subfacp1lem5  33146  cnpconn  33192  txsconnlem  33202  txsconn  33203  cvmliftmolem1  33243  cvmliftlem7  33253  cvmlift2lem3  33267  cvmlift2lem7  33271  cvmlift2lem9  33273  cvmliftphtlem  33279  cvmlift3lem1  33281  cvmlift3lem2  33282  cvmlift3lem4  33284  cvmlift3lem5  33285  cvmlift3lem6  33286  cvmlift3lem7  33287  mrsubco  33483  msubco  33493  mclsppslem  33545  sinccvglem  33630  iprodefisumlem  33706  iprodefisum  33707  poimirlem22  35799  mblfinlem2  35815  ftc1anclem5  35854  ftc1anclem8  35857  cocanfo  35876  f1ocan1fv  35884  upixp  35887  ghomco  36049  rngohomco  36132  lautco  38111  ldilco  38130  ltrncoval  38159  tendocoval  38780  tendoconid  38843  tendospass  39033  dicvscacl  39205  cdlemn3  39211  cdlemn9  39219  brcoffn  41640  fvovco  42732  climexp  43146  stoweidlem27  43568  stoweidlem31  43572  ovolval4lem1  44187  isomushgr  45278  mgmhmco  45355