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

Theorem fvco3 5596
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 5389 . 2  |-  ( G : A --> B  ->  G  Fn  A )
2 fvco2 5594 . 2  |-  ( ( G  Fn  A  /\  C  e.  A )  ->  ( ( F  o.  G ) `  C
)  =  ( F `
 ( G `  C ) ) )
31, 2sylan 457 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 358    = wceq 1623    e. wcel 1684    o. ccom 4693    Fn wfn 5250   -->wf 5251   ` cfv 5255
This theorem is referenced by:  foco2  5680  f1ocnvfv1  5792  f1ocnvfv2  5793  fcof1  5797  fcofo  5798  cocan1  5801  cocan2  5802  fveqf1o  5806  isotr  5833  algrflem  6224  fipreima  7161  unxpwdom2  7302  wemapwe  7400  ackbij2lem2  7866  cofsmo  7895  cfcoflem  7898  isf32lem6  7984  isf32lem7  7985  isf32lem8  7986  isf34lem7  8005  isf34lem6  8006  axcc3  8064  axdc4lem  8081  canthp1lem2  8275  inar1  8397  axdc4uzlem  11044  seqf1olem2  11086  seqf1o  11087  lo1o1  12006  o1co  12060  caucvgrlem2  12147  summolem3  12187  fsumf1o  12196  fsumcl2lem  12204  fsumadd  12211  fsummulc2  12246  fsumrelem  12265  supcvg  12314  ruclem11  12518  ruclem12  12519  algcvg  12746  eulerthlem2  12850  cofu1  13758  cofu2  13760  cofucl  13762  fucidcl  13839  fuclid  13840  fucrid  13841  homadm  13872  homacd  13873  evlfcl  13996  curfuncf  14012  yonedalem4c  14051  yonedalem3b  14053  yonedainv  14055  mhmco  14439  prdspjmhm  14443  pwsco1mhm  14446  lactghmga  14784  frgpup3lem  15086  gsumval3eu  15190  gsumval3  15191  gsumzaddlem  15203  gsumzmhm  15210  gsumzinv  15217  gsumsub  15219  dprdf1o  15267  mplsubglem  16179  gsumfsum  16439  frgpcyg  16527  cnpco  16996  lmcnp  17032  upxp  17317  uptx  17319  cnmpt11  17357  cnmpt21  17365  xkofvcn  17378  prdstmdd  17806  prdstgpd  17807  comet  18059  prdsxmslem2  18075  nrmmetd  18097  isngp3  18120  ngpds  18125  tngnm  18167  nmoco  18246  cnmetdval  18280  climcncf  18404  cncfco  18411  htpyco1  18476  htpyco2  18477  phtpyco2  18488  reparphti  18495  copco  18516  pi1cof  18557  pi1coghm  18559  caubl  18733  caublcls  18734  cniccbdd  18821  ovolfioo  18827  ovolficc  18828  ovolfsval  18830  ovolicc2lem1  18876  ovolicc2lem4  18879  ovolicc2lem5  18880  volsup  18913  uniiccdif  18933  uniioovol  18934  uniiccvol  18935  uniioombllem2  18938  uniioombllem3a  18939  uniioombllem4  18941  uniioombllem5  18942  mbfimaopnlem  19010  limccnp  19241  dvcobr  19295  dvcjbr  19298  dvfre  19300  evlssca  19406  evl1val  19411  plycjlem  19657  plycj  19658  coecj  19659  radcnvlem2  19790  radcnvlem3  19791  radcnvlt2  19795  pserulm  19798  resinf1o  19898  jensen  20283  ftalem3  20312  dchrinv  20500  dchr2sum  20512  dchrisum0re  20662  ex-co  20825  vafval  21159  smfval  21161  vsfval  21191  imsdval  21255  lnocoi  21335  occllem  21882  hocoi  22344  homco1  22381  counop  22501  homco2  22557  hmopco  22603  nlelchi  22641  kbass2  22697  kbass5  22700  leopsq  22709  hmopidmchi  22731  elpjrn  22770  pjinvari  22771  derangenlem  23702  subfacp1lem5  23715  cnpcon  23761  txsconlem  23771  txscon  23772  cvmliftmolem1  23812  cvmliftlem7  23822  cvmlift2lem3  23836  cvmlift2lem7  23840  cvmlift2lem9  23842  cvmliftphtlem  23848  cvmlift3lem1  23850  cvmlift3lem2  23851  cvmlift3lem4  23853  cvmlift3lem5  23854  cvmlift3lem6  23855  cvmlift3lem7  23856  sinccvglem  24005  surjsec2  25120  domval  25723  codval  25724  idval  25725  cmpval  25726  prismorcset2  25918  domcatfun  25925  codcatfun  25934  domidmor  25948  codidmor  25950  cmp2morpdom  25964  cmp2morpcod  25965  morexcmp  25967  cocanfo  26374  f1ocan1fv  26394  upixp  26403  ghomco  26573  rngohomco  26605  climexp  27731  stoweidlem27  27776  stoweidlem31  27780  lautco  30286  ldilco  30305  ltrncoval  30334  tendocoval  30955  tendoconid  31018  tendospass  31209  dicvscacl  31381  cdlemn3  31387  cdlemn9  31395
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-fv 5263
  Copyright terms: Public domain W3C validator