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

Theorem fvco3 5956
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 5744 . 2  |-  ( G : A --> B  ->  G  Fn  A )
2 fvco2 5954 . 2  |-  ( ( G  Fn  A  /\  C  e.  A )  ->  ( ( F  o.  G ) `  C
)  =  ( F `
 ( G `  C ) ) )
31, 2sylan 474 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 371    = wceq 1438    e. wcel 1869    o. ccom 4855    Fn wfn 5594   -->wf 5595   ` cfv 5599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-sbc 3301  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-uni 4218  df-br 4422  df-opab 4481  df-id 4766  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-fv 5607
This theorem is referenced by:  foco2  6055  f1ocnvfv1  6188  f1ocnvfv2  6189  fcof1  6198  fcofo  6199  cocan1  6202  cocan2  6203  fveqf1o  6213  isotr  6240  algrflem  6914  fipreima  7884  fsuppco2  7920  fsuppcor  7921  unxpwdom2  8107  wemapwe  8205  ackbij2lem2  8672  cofsmo  8701  cfcoflem  8704  isf32lem6  8790  isf32lem7  8791  isf32lem8  8792  isf34lem7  8811  isf34lem6  8812  axcc3  8870  axdc4lem  8887  canthp1lem2  9080  inar1  9202  axdc4uzlem  12196  seqf1olem2  12254  seqf1o  12255  lswco  12931  lo1o1  13589  o1co  13643  caucvgrlem2  13733  summolem3  13773  fsumf1o  13782  fsumcl2lem  13790  fsumadd  13798  fsummulc2  13838  fsumrelem  13860  supcvg  13907  prodmolem3  13980  fprodf1o  13993  fprodser  13996  fprodcl2lem  13997  fprodmul  14007  fproddiv  14008  fprodn0  14026  ruclem11  14285  ruclem12  14286  algcvg  14528  eulerthlem2  14723  cofu1  15782  cofu2  15784  cofucl  15786  fucidcl  15863  fuclid  15864  fucrid  15865  homadm  15928  homacd  15929  evlfcl  16100  curfuncf  16116  yonedalem4c  16155  yonedalem3b  16157  yonedainv  16159  mhmco  16602  prdspjmhm  16607  pwsco1mhm  16610  lactghmga  17038  frgpup3lem  17420  gsumval3eu  17531  gsumval3  17534  gsumzaddlem  17547  gsumzmhm  17563  dprdf1o  17658  mplsubglem  18651  evlssca  18738  evls1val  18902  evls1sca  18905  evl1val  18910  gsumfsum  19027  frgpcyg  19136  zrhpsgninv  19145  zrhpsgnevpm  19151  zrhpsgnodpm  19152  mdetralt  19625  mdetunilem7  19635  cpmadumatpoly  19899  chcoeffeqlem  19901  cnpco  20275  lmcnp  20312  upxp  20630  uptx  20632  cnmpt11  20670  cnmpt21  20678  xkofvcn  20691  prdstmdd  21130  prdstgpd  21131  comet  21520  prdsxmslem2  21536  nrmmetd  21581  isngp3  21604  ngpds  21609  tngnm  21651  nmoco  21750  cnmetdval  21783  climcncf  21924  cncfco  21931  htpyco1  22001  htpyco2  22002  phtpyco2  22013  reparphti  22020  copco  22041  pi1cof  22082  pi1coghm  22084  caubl  22269  caublcls  22270  cniccbdd  22404  ovolfioo  22412  ovolficc  22413  ovolfsval  22415  ovolicc2lem1  22462  ovolicc2lem4OLD  22465  ovolicc2lem4  22466  ovolicc2lem5  22467  volsup  22501  uniiccdif  22527  uniioovol  22528  uniiccvol  22529  uniioombllem2  22532  uniioombllem2OLD  22533  uniioombllem3a  22534  uniioombllem4  22536  uniioombllem5  22537  mbfimaopnlem  22603  limccnp  22838  dvcobr  22892  dvcjbr  22895  dvfre  22897  plycjlem  23222  plycj  23223  coecj  23224  radcnvlem2  23361  radcnvlem3  23362  radcnvlt2  23366  pserulm  23369  resinf1o  23477  jensen  23906  eflgam  23962  ftalem3  23991  dchrinv  24181  dchr2sum  24193  dchrisum0re  24343  motco  24577  motcgrg  24581  ex-co  25880  vafval  26214  smfval  26216  vsfval  26246  imsdval  26310  lnocoi  26390  occllem  26948  hocoi  27409  homco1  27446  counop  27566  homco2  27622  hmopco  27668  nlelchi  27706  kbass2  27762  kbass5  27765  leopsq  27774  hmopidmchi  27796  elpjrn  27835  pjinvari  27836  derangenlem  29896  subfacp1lem5  29909  cnpcon  29955  txsconlem  29965  txscon  29966  cvmliftmolem1  30006  cvmliftlem7  30016  cvmlift2lem3  30030  cvmlift2lem7  30034  cvmlift2lem9  30036  cvmliftphtlem  30042  cvmlift3lem1  30044  cvmlift3lem2  30045  cvmlift3lem4  30047  cvmlift3lem5  30048  cvmlift3lem6  30049  cvmlift3lem7  30050  mrsubco  30161  msubco  30171  mclsppslem  30223  sinccvglem  30318  iprodefisumlem  30377  iprodefisum  30378  poimirlem22  31920  mblfinlem2  31936  ftc1anclem5  31979  ftc1anclem8  31982  cocanfo  32002  f1ocan1fv  32011  upixp  32014  ghomco  32139  rngohomco  32171  lautco  33625  ldilco  33644  ltrncoval  33673  tendocoval  34296  tendoconid  34359  tendospass  34550  dicvscacl  34722  cdlemn3  34728  cdlemn9  34736  fvco3d  36506  fvovco  37363  climexp  37547  stoweidlem27  37751  stoweidlem31  37756  mgmhmco  39143
  Copyright terms: Public domain W3C validator