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

Theorem fvco3 5926
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 5714 . 2  |-  ( G : A --> B  ->  G  Fn  A )
2 fvco2 5924 . 2  |-  ( ( G  Fn  A  /\  C  e.  A )  ->  ( ( F  o.  G ) `  C
)  =  ( F `
 ( G `  C ) ) )
31, 2sylan 469 1  |-  ( ( G : A --> B  /\  C  e.  A )  ->  ( ( F  o.  G ) `  C
)  =  ( F `
 ( G `  C ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1405    e. wcel 1842    o. ccom 4827    Fn wfn 5564   -->wf 5565   ` cfv 5569
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-rab 2763  df-v 3061  df-sbc 3278  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4192  df-br 4396  df-opab 4454  df-id 4738  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-iota 5533  df-fun 5571  df-fn 5572  df-f 5573  df-fv 5577
This theorem is referenced by:  foco2  6029  f1ocnvfv1  6163  f1ocnvfv2  6164  fcof1  6173  fcofo  6174  cocan1  6177  cocan2  6178  fveqf1o  6188  isotr  6215  algrflem  6893  fipreima  7860  fsuppco2  7896  fsuppcor  7897  unxpwdom2  8048  wemapwe  8171  wemapweOLD  8172  ackbij2lem2  8652  cofsmo  8681  cfcoflem  8684  isf32lem6  8770  isf32lem7  8771  isf32lem8  8772  isf34lem7  8791  isf34lem6  8792  axcc3  8850  axdc4lem  8867  canthp1lem2  9061  inar1  9183  axdc4uzlem  12133  seqf1olem2  12191  seqf1o  12192  lswco  12860  lo1o1  13504  o1co  13558  caucvgrlem2  13646  summolem3  13685  fsumf1o  13694  fsumcl2lem  13702  fsumadd  13710  fsummulc2  13750  fsumrelem  13772  supcvg  13819  prodmolem3  13892  fprodf1o  13905  fprodser  13908  fprodcl2lem  13909  fprodmul  13917  fproddiv  13918  fprodn0  13935  ruclem11  14182  ruclem12  14183  algcvg  14414  eulerthlem2  14521  cofu1  15497  cofu2  15499  cofucl  15501  fucidcl  15578  fuclid  15579  fucrid  15580  homadm  15643  homacd  15644  evlfcl  15815  curfuncf  15831  yonedalem4c  15870  yonedalem3b  15872  yonedainv  15874  mhmco  16317  prdspjmhm  16322  pwsco1mhm  16325  lactghmga  16753  frgpup3lem  17119  gsumval3eu  17231  gsumval3OLD  17232  gsumval3  17235  gsumzaddlem  17258  gsumzaddlemOLD  17260  gsumzmhm  17280  gsumzmhmOLD  17281  gsumzinvOLD  17293  dprdf1o  17399  mplsubglem  18413  mplsubglemOLD  18415  evlssca  18511  evls1val  18677  evls1sca  18680  evl1val  18685  gsumfsum  18804  frgpcyg  18910  zrhpsgninv  18919  zrhpsgnevpm  18925  zrhpsgnodpm  18926  mdetralt  19402  mdetunilem7  19412  cpmadumatpoly  19676  chcoeffeqlem  19678  cnpco  20061  lmcnp  20098  upxp  20416  uptx  20418  cnmpt11  20456  cnmpt21  20464  xkofvcn  20477  prdstmdd  20914  prdstgpd  20915  comet  21308  prdsxmslem2  21324  nrmmetd  21387  isngp3  21410  ngpds  21415  tngnm  21457  nmoco  21536  cnmetdval  21570  climcncf  21696  cncfco  21703  htpyco1  21770  htpyco2  21771  phtpyco2  21782  reparphti  21789  copco  21810  pi1cof  21851  pi1coghm  21853  caubl  22038  caublcls  22039  cniccbdd  22165  ovolfioo  22171  ovolficc  22172  ovolfsval  22174  ovolicc2lem1  22220  ovolicc2lem4  22223  ovolicc2lem5  22224  volsup  22258  uniiccdif  22279  uniioovol  22280  uniiccvol  22281  uniioombllem2  22284  uniioombllem3a  22285  uniioombllem4  22287  uniioombllem5  22288  mbfimaopnlem  22354  limccnp  22587  dvcobr  22641  dvcjbr  22644  dvfre  22646  plycjlem  22965  plycj  22966  coecj  22967  radcnvlem2  23101  radcnvlem3  23102  radcnvlt2  23106  pserulm  23109  resinf1o  23215  jensen  23644  eflgam  23700  ftalem3  23729  dchrinv  23917  dchr2sum  23929  dchrisum0re  24079  motco  24310  motcgrg  24314  ex-co  25576  vafval  25910  smfval  25912  vsfval  25942  imsdval  26006  lnocoi  26086  occllem  26635  hocoi  27096  homco1  27133  counop  27253  homco2  27309  hmopco  27355  nlelchi  27393  kbass2  27449  kbass5  27452  leopsq  27461  hmopidmchi  27483  elpjrn  27522  pjinvari  27523  derangenlem  29468  subfacp1lem5  29481  cnpcon  29527  txsconlem  29537  txscon  29538  cvmliftmolem1  29578  cvmliftlem7  29588  cvmlift2lem3  29602  cvmlift2lem7  29606  cvmlift2lem9  29608  cvmliftphtlem  29614  cvmlift3lem1  29616  cvmlift3lem2  29617  cvmlift3lem4  29619  cvmlift3lem5  29620  cvmlift3lem6  29621  cvmlift3lem7  29622  mrsubco  29733  msubco  29743  mclsppslem  29795  sinccvglem  29890  iprodefisumlem  29949  iprodefisum  29950  mblfinlem2  31424  ftc1anclem5  31467  ftc1anclem8  31470  cocanfo  31490  f1ocan1fv  31499  upixp  31502  ghomco  31627  rngohomco  31659  lautco  33114  ldilco  33133  ltrncoval  33162  tendocoval  33785  tendoconid  33848  tendospass  34039  dicvscacl  34211  cdlemn3  34217  cdlemn9  34225  fvco3d  35989  climexp  36979  stoweidlem27  37177  stoweidlem31  37181  mgmhmco  38118
  Copyright terms: Public domain W3C validator