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

Theorem fvco3 5867
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 5657 . 2  |-  ( G : A --> B  ->  G  Fn  A )
2 fvco2 5865 . 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 1370    e. wcel 1758    o. ccom 4942    Fn wfn 5511   -->wf 5512   ` cfv 5516
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-sbc 3285  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-opab 4449  df-id 4734  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-fv 5524
This theorem is referenced by:  foco2  5962  f1ocnvfv1  6082  f1ocnvfv2  6083  fcof1  6090  fcofo  6091  cocan1  6094  cocan2  6095  fveqf1o  6099  isotr  6126  algrflem  6781  fipreima  7718  fsuppco2  7753  fsuppcor  7754  unxpwdom2  7904  wemapwe  8029  wemapweOLD  8030  ackbij2lem2  8510  cofsmo  8539  cfcoflem  8542  isf32lem6  8628  isf32lem7  8629  isf32lem8  8630  isf34lem7  8649  isf34lem6  8650  axcc3  8708  axdc4lem  8725  canthp1lem2  8921  inar1  9043  axdc4uzlem  11905  seqf1olem2  11947  seqf1o  11948  lswco  12568  lo1o1  13112  o1co  13166  caucvgrlem2  13254  summolem3  13293  fsumf1o  13302  fsumcl2lem  13310  fsumadd  13317  fsummulc2  13353  fsumrelem  13372  supcvg  13420  ruclem11  13624  ruclem12  13625  algcvg  13853  eulerthlem2  13959  cofu1  14896  cofu2  14898  cofucl  14900  fucidcl  14977  fuclid  14978  fucrid  14979  homadm  15010  homacd  15011  evlfcl  15134  curfuncf  15150  yonedalem4c  15189  yonedalem3b  15191  yonedainv  15193  mhmco  15592  prdspjmhm  15597  pwsco1mhm  15600  lactghmga  16011  frgpup3lem  16378  gsumval3eu  16485  gsumval3OLD  16486  gsumval3  16489  gsumzaddlem  16512  gsumzaddlemOLD  16514  gsumzmhm  16535  gsumzmhmOLD  16536  gsumzinvOLD  16548  gsumsubOLD  16553  dprdf1o  16634  mplsubglem  17617  mplsubglemOLD  17619  evlssca  17715  evls1val  17864  evls1sca  17867  evl1val  17872  gsumfsum  17988  frgpcyg  18115  zrhpsgninv  18124  zrhpsgnevpm  18130  zrhpsgnodpm  18131  mdetralt  18530  mdetunilem7  18540  cnpco  18987  lmcnp  19024  upxp  19312  uptx  19314  cnmpt11  19352  cnmpt21  19360  xkofvcn  19373  prdstmdd  19810  prdstgpd  19811  comet  20204  prdsxmslem2  20220  nrmmetd  20283  isngp3  20306  ngpds  20311  tngnm  20353  nmoco  20432  cnmetdval  20466  climcncf  20592  cncfco  20599  htpyco1  20666  htpyco2  20667  phtpyco2  20678  reparphti  20685  copco  20706  pi1cof  20747  pi1coghm  20749  caubl  20934  caublcls  20935  cniccbdd  21061  ovolfioo  21067  ovolficc  21068  ovolfsval  21070  ovolicc2lem1  21116  ovolicc2lem4  21119  ovolicc2lem5  21120  volsup  21153  uniiccdif  21174  uniioovol  21175  uniiccvol  21176  uniioombllem2  21179  uniioombllem3a  21180  uniioombllem4  21182  uniioombllem5  21183  mbfimaopnlem  21249  limccnp  21482  dvcobr  21536  dvcjbr  21539  dvfre  21541  plycjlem  21859  plycj  21860  coecj  21861  radcnvlem2  21995  radcnvlem3  21996  radcnvlt2  22000  pserulm  22003  resinf1o  22108  jensen  22498  ftalem3  22528  dchrinv  22716  dchr2sum  22728  dchrisum0re  22878  ex-co  23780  vafval  24116  smfval  24118  vsfval  24148  imsdval  24212  lnocoi  24292  occllem  24841  hocoi  25303  homco1  25340  counop  25460  homco2  25516  hmopco  25562  nlelchi  25600  kbass2  25656  kbass5  25659  leopsq  25668  hmopidmchi  25690  elpjrn  25729  pjinvari  25730  eflgam  27165  derangenlem  27193  subfacp1lem5  27206  cnpcon  27253  txsconlem  27263  txscon  27264  cvmliftmolem1  27304  cvmliftlem7  27314  cvmlift2lem3  27328  cvmlift2lem7  27332  cvmlift2lem9  27334  cvmliftphtlem  27340  cvmlift3lem1  27342  cvmlift3lem2  27343  cvmlift3lem4  27345  cvmlift3lem5  27346  cvmlift3lem6  27347  cvmlift3lem7  27348  sinccvglem  27451  prodmolem3  27580  fprodf1o  27593  fprodser  27596  fprodcl2lem  27597  fprodmul  27605  fproddiv  27606  fprodn0  27624  iprodefisumlem  27638  iprodefisum  27639  mblfinlem2  28567  ftc1anclem5  28609  ftc1anclem8  28612  cocanfo  28749  f1ocan1fv  28758  upixp  28761  ghomco  28886  rngohomco  28918  climexp  29916  stoweidlem27  29960  stoweidlem31  29964  cpmadumatpoly  31338  chcoeffeqlem  31340  lautco  34047  ldilco  34066  ltrncoval  34095  tendocoval  34716  tendoconid  34779  tendospass  34970  dicvscacl  35142  cdlemn3  35148  cdlemn9  35156
  Copyright terms: Public domain W3C validator