Theorem fvco3 6760

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114   ∘ ccom 5559   Fn wfn 6350  ⟶wf 6351  ‘cfv 6355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-fv 6363

This theorem is referenced by:  fvco3d  6761  foco2  6873  f1cofveqaeqALT  7017  f1ocnvfv1  7033  f1ocnvfv2  7034  fcof1  7043  fcofo  7044  cocan1  7047  cocan2  7048  fveqf1o  7058  isotr  7089  algrflem  7819  fipreima  8830  fsuppco2  8866  fsuppcor  8867  unxpwdom2  9052  wemapwe  9160  ackbij2lem2  9662  cofsmo  9691  cfcoflem  9694  isf32lem6  9780  isf32lem7  9781  isf32lem8  9782  isf34lem7  9801  isf34lem6  9802  axcc3  9860  axdc4lem  9877  canthp1lem2  10075  inar1  10197  axdc4uzlem  13352  seqf1olem2  13411  seqf1o  13412  lswco  14201  lo1o1  14889  o1co  14943  caucvgrlem2  15031  summolem3  15071  fsumf1o  15080  fsumcl2lem  15088  fsumadd  15096  fsummulc2  15139  fsumrelem  15162  supcvg  15211  prodmolem3  15287  fprodf1o  15300  fprodser  15303  fprodcl2lem  15304  fprodmul  15314  fproddiv  15315  fprodn0  15333  ruclem11  15593  ruclem12  15594  algcvg  15920  eulerthlem2  16119  cofu1  17154  cofu2  17156  cofucl  17158  fucidcl  17235  fuclid  17236  fucrid  17237  homadm  17300  homacd  17301  evlfcl  17472  curfuncf  17488  yonedalem4c  17527  yonedalem3b  17529  mhmco  17988  prdspjmhm  17993  pwsco1mhm  17996  lactghmga  18533  frgpup3lem  18903  gsumval3eu  19024  gsumval3  19027  gsumzaddlem  19041  gsumzmhm  19057  dprdf1o  19154  mplsubglem  20214  evlssca  20302  evls1val  20483  evls1sca  20486  evl1val  20492  gsumfsum  20612  zrhpsgninv  20729  zrhpsgnevpm  20735  zrhpsgnodpm  20736  mdetralt  21217  mdetunilem7  21227  cpmadumatpoly  21491  chcoeffeqlem  21493  cnpco  21875  lmcnp  21912  upxp  22231  uptx  22233  cnmpt11  22271  cnmpt21  22279  xkofvcn  22292  prdstmdd  22732  prdstgpd  22733  comet  23123  prdsxmslem2  23139  nrmmetd  23184  isngp3  23207  ngpds  23213  tngnm  23260  nmoco  23346  cnmetdval  23379  climcncf  23508  cncfco  23515  htpyco1  23582  htpyco2  23583  phtpyco2  23594  reparphti  23601  copco  23622  pi1cof  23663  pi1coghm  23665  caubl  23911  caublcls  23912  cniccbdd  24062  ovolfioo  24068  ovolficc  24069  ovolfsval  24071  ovolicc2lem1  24118  ovolicc2lem4  24121  ovolicc2lem5  24122  volsup  24157  uniiccdif  24179  uniioovol  24180  uniiccvol  24181  uniioombllem2  24184  uniioombllem3a  24185  uniioombllem4  24187  uniioombllem5  24188  mbfimaopnlem  24256  limccnp  24489  dvcobr  24543  dvcjbr  24546  dvfre  24548  plycjlem  24866  plycj  24867  coecj  24868  radcnvlem2  25002  radcnvlem3  25003  radcnvlt2  25007  pserulm  25010  resinf1o  25120  jensen  25566  eflgam  25622  ftalem3  25652  dchrinv  25837  dchr2sum  25849  dchrisum0re  26089  motco  26326  motcgrg  26330  ex-co  28217  vafval  28380  smfval  28382  vsfval  28410  imsdval  28463  lnocoi  28534  occllem  29080  hocoi  29541  homco1  29578  counop  29698  homco2  29754  hmopco  29800  nlelchi  29838  kbass2  29894  kbass5  29897  leopsq  29906  hmopidmchi  29928  elpjrn  29967  pjinvari  29968  cycpmco2  30775  derangenlem  32418  subfacp1lem5  32431  cnpconn  32477  txsconnlem  32487  txsconn  32488  cvmliftmolem1  32528  cvmliftlem7  32538  cvmlift2lem3  32552  cvmlift2lem7  32556  cvmlift2lem9  32558  cvmliftphtlem  32564  cvmlift3lem1  32566  cvmlift3lem2  32567  cvmlift3lem4  32569  cvmlift3lem5  32570  cvmlift3lem6  32571  cvmlift3lem7  32572  mrsubco  32768  msubco  32778  mclsppslem  32830  sinccvglem  32915  iprodefisumlem  32972  iprodefisum  32973  poimirlem22  34929  mblfinlem2  34945  ftc1anclem5  34986  ftc1anclem8  34989  cocanfo  35008  f1ocan1fv  35016  upixp  35019  ghomco  35184  rngohomco  35267  lautco  37248  ldilco  37267  ltrncoval  37296  tendocoval  37917  tendoconid  37980  tendospass  38170  dicvscacl  38342  cdlemn3  38348  cdlemn9  38356  brcoffn  40400  fvovco  41475  climexp  41906  stoweidlem27  42332  stoweidlem31  42336  ovolval4lem1  42951  isomushgr  44011  mgmhmco  44088