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

Theorem fvco3 5950
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 5737 . 2  |-  ( G : A --> B  ->  G  Fn  A )
2 fvco2 5948 . 2  |-  ( ( G  Fn  A  /\  C  e.  A )  ->  ( ( F  o.  G ) `  C
)  =  ( F `
 ( G `  C ) ) )
31, 2sylan 471 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 369    = wceq 1395    e. wcel 1819    o. ccom 5012    Fn wfn 5589   -->wf 5590   ` cfv 5594
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-opab 4516  df-id 4804  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-fv 5602
This theorem is referenced by:  foco2  6052  f1ocnvfv1  6183  f1ocnvfv2  6184  fcof1  6191  fcofo  6192  cocan1  6195  cocan2  6196  fveqf1o  6206  isotr  6233  algrflem  6908  fipreima  7844  fsuppco2  7880  fsuppcor  7881  unxpwdom2  8032  wemapwe  8156  wemapweOLD  8157  ackbij2lem2  8637  cofsmo  8666  cfcoflem  8669  isf32lem6  8755  isf32lem7  8756  isf32lem8  8757  isf34lem7  8776  isf34lem6  8777  axcc3  8835  axdc4lem  8852  canthp1lem2  9048  inar1  9170  axdc4uzlem  12095  seqf1olem2  12150  seqf1o  12151  lswco  12816  lo1o1  13367  o1co  13421  caucvgrlem2  13509  summolem3  13548  fsumf1o  13557  fsumcl2lem  13565  fsumadd  13573  fsummulc2  13611  fsumrelem  13633  supcvg  13679  prodmolem3  13752  fprodf1o  13765  fprodser  13768  fprodcl2lem  13769  fprodmul  13777  fproddiv  13778  fprodn0  13795  ruclem11  13985  ruclem12  13986  algcvg  14217  eulerthlem2  14324  cofu1  15300  cofu2  15302  cofucl  15304  fucidcl  15381  fuclid  15382  fucrid  15383  homadm  15446  homacd  15447  evlfcl  15618  curfuncf  15634  yonedalem4c  15673  yonedalem3b  15675  yonedainv  15677  mhmco  16120  prdspjmhm  16125  pwsco1mhm  16128  lactghmga  16556  frgpup3lem  16922  gsumval3eu  17034  gsumval3OLD  17035  gsumval3  17038  gsumzaddlem  17061  gsumzaddlemOLD  17063  gsumzmhm  17084  gsumzmhmOLD  17085  gsumzinvOLD  17097  gsumsubOLD  17102  dprdf1o  17206  mplsubglem  18220  mplsubglemOLD  18222  evlssca  18318  evls1val  18484  evls1sca  18487  evl1val  18492  gsumfsum  18611  frgpcyg  18739  zrhpsgninv  18748  zrhpsgnevpm  18754  zrhpsgnodpm  18755  mdetralt  19237  mdetunilem7  19247  cpmadumatpoly  19511  chcoeffeqlem  19513  cnpco  19895  lmcnp  19932  upxp  20250  uptx  20252  cnmpt11  20290  cnmpt21  20298  xkofvcn  20311  prdstmdd  20748  prdstgpd  20749  comet  21142  prdsxmslem2  21158  nrmmetd  21221  isngp3  21244  ngpds  21249  tngnm  21291  nmoco  21370  cnmetdval  21404  climcncf  21530  cncfco  21537  htpyco1  21604  htpyco2  21605  phtpyco2  21616  reparphti  21623  copco  21644  pi1cof  21685  pi1coghm  21687  caubl  21872  caublcls  21873  cniccbdd  21999  ovolfioo  22005  ovolficc  22006  ovolfsval  22008  ovolicc2lem1  22054  ovolicc2lem4  22057  ovolicc2lem5  22058  volsup  22092  uniiccdif  22113  uniioovol  22114  uniiccvol  22115  uniioombllem2  22118  uniioombllem3a  22119  uniioombllem4  22121  uniioombllem5  22122  mbfimaopnlem  22188  limccnp  22421  dvcobr  22475  dvcjbr  22478  dvfre  22480  plycjlem  22799  plycj  22800  coecj  22801  radcnvlem2  22935  radcnvlem3  22936  radcnvlt2  22940  pserulm  22943  resinf1o  23049  jensen  23444  ftalem3  23474  dchrinv  23662  dchr2sum  23674  dchrisum0re  23824  motco  24053  motcgrg  24057  ex-co  25286  vafval  25623  smfval  25625  vsfval  25655  imsdval  25719  lnocoi  25799  occllem  26348  hocoi  26810  homco1  26847  counop  26967  homco2  27023  hmopco  27069  nlelchi  27107  kbass2  27163  kbass5  27166  leopsq  27175  hmopidmchi  27197  elpjrn  27236  pjinvari  27237  eflgam  28784  derangenlem  28812  subfacp1lem5  28825  cnpcon  28872  txsconlem  28882  txscon  28883  cvmliftmolem1  28923  cvmliftlem7  28933  cvmlift2lem3  28947  cvmlift2lem7  28951  cvmlift2lem9  28953  cvmliftphtlem  28959  cvmlift3lem1  28961  cvmlift3lem2  28962  cvmlift3lem4  28964  cvmlift3lem5  28965  cvmlift3lem6  28966  cvmlift3lem7  28967  mrsubco  29078  msubco  29088  mclsppslem  29140  sinccvglem  29235  iprodefisumlem  29341  iprodefisum  29342  mblfinlem2  30257  ftc1anclem5  30299  ftc1anclem8  30302  cocanfo  30413  f1ocan1fv  30422  upixp  30425  ghomco  30550  rngohomco  30582  climexp  31814  stoweidlem27  32012  stoweidlem31  32016  mgmhmco  32751  lautco  35964  ldilco  35983  ltrncoval  36012  tendocoval  36635  tendoconid  36698  tendospass  36889  dicvscacl  37061  cdlemn3  37067  cdlemn9  37075  fvco3d  38170
  Copyright terms: Public domain W3C validator