MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvco3 Unicode version

Theorem fvco3 5759
Description: Value of a function composition. (Contributed by NM, 3-Jan-2004.) (Revised by Mario Carneiro, 26-Dec-2014.)
Assertion
Ref Expression
fvco3  |-  ( ( G : A --> B  /\  C  e.  A )  ->  ( ( F  o.  G ) `  C
)  =  ( F `
 ( G `  C ) ) )

Proof of Theorem fvco3
StepHypRef Expression
1 ffn 5550 . 2  |-  ( G : A --> B  ->  G  Fn  A )
2 fvco2 5757 . 2  |-  ( ( G  Fn  A  /\  C  e.  A )  ->  ( ( F  o.  G ) `  C
)  =  ( F `
 ( G `  C ) ) )
31, 2sylan 458 1  |-  ( ( G : A --> B  /\  C  e.  A )  ->  ( ( F  o.  G ) `  C
)  =  ( F `
 ( G `  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1721    o. ccom 4841    Fn wfn 5408   -->wf 5409   ` cfv 5413
This theorem is referenced by:  foco2  5848  f1ocnvfv1  5973  f1ocnvfv2  5974  fcof1  5979  fcofo  5980  cocan1  5983  cocan2  5984  fveqf1o  5988  isotr  6015  algrflem  6414  fipreima  7370  unxpwdom2  7512  wemapwe  7610  ackbij2lem2  8076  cofsmo  8105  cfcoflem  8108  isf32lem6  8194  isf32lem7  8195  isf32lem8  8196  isf34lem7  8215  isf34lem6  8216  axcc3  8274  axdc4lem  8291  canthp1lem2  8484  inar1  8606  axdc4uzlem  11276  seqf1olem2  11318  seqf1o  11319  lo1o1  12281  o1co  12335  caucvgrlem2  12423  summolem3  12463  fsumf1o  12472  fsumcl2lem  12480  fsumadd  12487  fsummulc2  12522  fsumrelem  12541  supcvg  12590  ruclem11  12794  ruclem12  12795  algcvg  13022  eulerthlem2  13126  cofu1  14036  cofu2  14038  cofucl  14040  fucidcl  14117  fuclid  14118  fucrid  14119  homadm  14150  homacd  14151  evlfcl  14274  curfuncf  14290  yonedalem4c  14329  yonedalem3b  14331  yonedainv  14333  mhmco  14717  prdspjmhm  14721  pwsco1mhm  14724  lactghmga  15062  frgpup3lem  15364  gsumval3eu  15468  gsumval3  15469  gsumzaddlem  15481  gsumzmhm  15488  gsumzinv  15495  gsumsub  15497  dprdf1o  15545  mplsubglem  16453  gsumfsum  16721  frgpcyg  16809  cnpco  17285  lmcnp  17322  upxp  17608  uptx  17610  cnmpt11  17648  cnmpt21  17656  xkofvcn  17669  prdstmdd  18106  prdstgpd  18107  comet  18496  prdsxmslem2  18512  nrmmetd  18575  isngp3  18598  ngpds  18603  tngnm  18645  nmoco  18724  cnmetdval  18758  climcncf  18883  cncfco  18890  htpyco1  18956  htpyco2  18957  phtpyco2  18968  reparphti  18975  copco  18996  pi1cof  19037  pi1coghm  19039  caubl  19213  caublcls  19214  cniccbdd  19311  ovolfioo  19317  ovolficc  19318  ovolfsval  19320  ovolicc2lem1  19366  ovolicc2lem4  19369  ovolicc2lem5  19370  volsup  19403  uniiccdif  19423  uniioovol  19424  uniiccvol  19425  uniioombllem2  19428  uniioombllem3a  19429  uniioombllem4  19431  uniioombllem5  19432  mbfimaopnlem  19500  limccnp  19731  dvcobr  19785  dvcjbr  19788  dvfre  19790  evlssca  19896  evl1val  19901  plycjlem  20147  plycj  20148  coecj  20149  radcnvlem2  20283  radcnvlem3  20284  radcnvlt2  20288  pserulm  20291  resinf1o  20391  jensen  20780  ftalem3  20810  dchrinv  20998  dchr2sum  21010  dchrisum0re  21160  ex-co  21699  vafval  22035  smfval  22037  vsfval  22067  imsdval  22131  lnocoi  22211  occllem  22758  hocoi  23220  homco1  23257  counop  23377  homco2  23433  hmopco  23479  nlelchi  23517  kbass2  23573  kbass5  23576  leopsq  23585  hmopidmchi  23607  elpjrn  23646  pjinvari  23647  eflgam  24782  derangenlem  24810  subfacp1lem5  24823  cnpcon  24870  txsconlem  24880  txscon  24881  cvmliftmolem1  24921  cvmliftlem7  24931  cvmlift2lem3  24945  cvmlift2lem7  24949  cvmlift2lem9  24951  cvmliftphtlem  24957  cvmlift3lem1  24959  cvmlift3lem2  24960  cvmlift3lem4  24962  cvmlift3lem5  24963  cvmlift3lem6  24964  cvmlift3lem7  24965  sinccvglem  25062  prodmolem3  25212  fprodf1o  25225  fprodser  25228  fprodcl2lem  25229  fprodmul  25237  fproddiv  25238  fprodn0  25256  iprodefisumlem  25270  iprodefisum  25271  mblfinlem  26143  cocanfo  26309  f1ocan1fv  26318  upixp  26321  ghomco  26448  rngohomco  26480  climexp  27598  stoweidlem27  27643  stoweidlem31  27647  lautco  30579  ldilco  30598  ltrncoval  30627  tendocoval  31248  tendoconid  31311  tendospass  31502  dicvscacl  31674  cdlemn3  31680  cdlemn9  31688
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-fv 5421
  Copyright terms: Public domain W3C validator