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

Theorem fvco3 5802
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 5593 . 2  |-  ( G : A --> B  ->  G  Fn  A )
2 fvco2 5800 . 2  |-  ( ( G  Fn  A  /\  C  e.  A )  ->  ( ( F  o.  G ) `  C
)  =  ( F `
 ( G `  C ) ) )
31, 2sylan 459 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 360    = wceq 1653    e. wcel 1726    o. ccom 4884    Fn wfn 5451   -->wf 5452   ` cfv 5456
This theorem is referenced by:  foco2  5891  f1ocnvfv1  6016  f1ocnvfv2  6017  fcof1  6022  fcofo  6023  cocan1  6026  cocan2  6027  fveqf1o  6031  isotr  6058  algrflem  6457  fipreima  7414  unxpwdom2  7558  wemapwe  7656  ackbij2lem2  8122  cofsmo  8151  cfcoflem  8154  isf32lem6  8240  isf32lem7  8241  isf32lem8  8242  isf34lem7  8261  isf34lem6  8262  axcc3  8320  axdc4lem  8337  canthp1lem2  8530  inar1  8652  axdc4uzlem  11323  seqf1olem2  11365  seqf1o  11366  lo1o1  12328  o1co  12382  caucvgrlem2  12470  summolem3  12510  fsumf1o  12519  fsumcl2lem  12527  fsumadd  12534  fsummulc2  12569  fsumrelem  12588  supcvg  12637  ruclem11  12841  ruclem12  12842  algcvg  13069  eulerthlem2  13173  cofu1  14083  cofu2  14085  cofucl  14087  fucidcl  14164  fuclid  14165  fucrid  14166  homadm  14197  homacd  14198  evlfcl  14321  curfuncf  14337  yonedalem4c  14376  yonedalem3b  14378  yonedainv  14380  mhmco  14764  prdspjmhm  14768  pwsco1mhm  14771  lactghmga  15109  frgpup3lem  15411  gsumval3eu  15515  gsumval3  15516  gsumzaddlem  15528  gsumzmhm  15535  gsumzinv  15542  gsumsub  15544  dprdf1o  15592  mplsubglem  16500  gsumfsum  16768  frgpcyg  16856  cnpco  17333  lmcnp  17370  upxp  17657  uptx  17659  cnmpt11  17697  cnmpt21  17705  xkofvcn  17718  prdstmdd  18155  prdstgpd  18156  comet  18545  prdsxmslem2  18561  nrmmetd  18624  isngp3  18647  ngpds  18652  tngnm  18694  nmoco  18773  cnmetdval  18807  climcncf  18932  cncfco  18939  htpyco1  19005  htpyco2  19006  phtpyco2  19017  reparphti  19024  copco  19045  pi1cof  19086  pi1coghm  19088  caubl  19262  caublcls  19263  cniccbdd  19360  ovolfioo  19366  ovolficc  19367  ovolfsval  19369  ovolicc2lem1  19415  ovolicc2lem4  19418  ovolicc2lem5  19419  volsup  19452  uniiccdif  19472  uniioovol  19473  uniiccvol  19474  uniioombllem2  19477  uniioombllem3a  19478  uniioombllem4  19480  uniioombllem5  19481  mbfimaopnlem  19549  limccnp  19780  dvcobr  19834  dvcjbr  19837  dvfre  19839  evlssca  19945  evl1val  19950  plycjlem  20196  plycj  20197  coecj  20198  radcnvlem2  20332  radcnvlem3  20333  radcnvlt2  20337  pserulm  20340  resinf1o  20440  jensen  20829  ftalem3  20859  dchrinv  21047  dchr2sum  21059  dchrisum0re  21209  ex-co  21748  vafval  22084  smfval  22086  vsfval  22116  imsdval  22180  lnocoi  22260  occllem  22807  hocoi  23269  homco1  23306  counop  23426  homco2  23482  hmopco  23528  nlelchi  23566  kbass2  23622  kbass5  23625  leopsq  23634  hmopidmchi  23656  elpjrn  23695  pjinvari  23696  eflgam  24831  derangenlem  24859  subfacp1lem5  24872  cnpcon  24919  txsconlem  24929  txscon  24930  cvmliftmolem1  24970  cvmliftlem7  24980  cvmlift2lem3  24994  cvmlift2lem7  24998  cvmlift2lem9  25000  cvmliftphtlem  25006  cvmlift3lem1  25008  cvmlift3lem2  25009  cvmlift3lem4  25011  cvmlift3lem5  25012  cvmlift3lem6  25013  cvmlift3lem7  25014  sinccvglem  25111  prodmolem3  25261  fprodf1o  25274  fprodser  25277  fprodcl2lem  25278  fprodmul  25286  fproddiv  25287  fprodn0  25305  iprodefisumlem  25319  iprodefisum  25320  mblfinlem2  26246  ftc1anclem5  26286  ftc1anclem8  26289  cocanfo  26421  f1ocan1fv  26430  upixp  26433  ghomco  26560  rngohomco  26592  climexp  27709  stoweidlem27  27754  stoweidlem31  27758  lautco  30956  ldilco  30975  ltrncoval  31004  tendocoval  31625  tendoconid  31688  tendospass  31879  dicvscacl  32051  cdlemn3  32057  cdlemn9  32065
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332  ax-nul 4340  ax-pow 4379  ax-pr 4405
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4215  df-opab 4269  df-id 4500  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-fv 5464
  Copyright terms: Public domain W3C validator