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

Theorem fvco3 5793
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 5584 . 2  |-  ( G : A --> B  ->  G  Fn  A )
2 fvco2 5791 . 2  |-  ( ( G  Fn  A  /\  C  e.  A )  ->  ( ( F  o.  G ) `  C
)  =  ( F `
 ( G `  C ) ) )
31, 2sylan 458 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 359    = wceq 1652    e. wcel 1725    o. ccom 4875    Fn wfn 5442   -->wf 5443   ` cfv 5447
This theorem is referenced by:  foco2  5882  f1ocnvfv1  6007  f1ocnvfv2  6008  fcof1  6013  fcofo  6014  cocan1  6017  cocan2  6018  fveqf1o  6022  isotr  6049  algrflem  6448  fipreima  7405  unxpwdom2  7549  wemapwe  7647  ackbij2lem2  8113  cofsmo  8142  cfcoflem  8145  isf32lem6  8231  isf32lem7  8232  isf32lem8  8233  isf34lem7  8252  isf34lem6  8253  axcc3  8311  axdc4lem  8328  canthp1lem2  8521  inar1  8643  axdc4uzlem  11314  seqf1olem2  11356  seqf1o  11357  lo1o1  12319  o1co  12373  caucvgrlem2  12461  summolem3  12501  fsumf1o  12510  fsumcl2lem  12518  fsumadd  12525  fsummulc2  12560  fsumrelem  12579  supcvg  12628  ruclem11  12832  ruclem12  12833  algcvg  13060  eulerthlem2  13164  cofu1  14074  cofu2  14076  cofucl  14078  fucidcl  14155  fuclid  14156  fucrid  14157  homadm  14188  homacd  14189  evlfcl  14312  curfuncf  14328  yonedalem4c  14367  yonedalem3b  14369  yonedainv  14371  mhmco  14755  prdspjmhm  14759  pwsco1mhm  14762  lactghmga  15100  frgpup3lem  15402  gsumval3eu  15506  gsumval3  15507  gsumzaddlem  15519  gsumzmhm  15526  gsumzinv  15533  gsumsub  15535  dprdf1o  15583  mplsubglem  16491  gsumfsum  16759  frgpcyg  16847  cnpco  17324  lmcnp  17361  upxp  17648  uptx  17650  cnmpt11  17688  cnmpt21  17696  xkofvcn  17709  prdstmdd  18146  prdstgpd  18147  comet  18536  prdsxmslem2  18552  nrmmetd  18615  isngp3  18638  ngpds  18643  tngnm  18685  nmoco  18764  cnmetdval  18798  climcncf  18923  cncfco  18930  htpyco1  18996  htpyco2  18997  phtpyco2  19008  reparphti  19015  copco  19036  pi1cof  19077  pi1coghm  19079  caubl  19253  caublcls  19254  cniccbdd  19351  ovolfioo  19357  ovolficc  19358  ovolfsval  19360  ovolicc2lem1  19406  ovolicc2lem4  19409  ovolicc2lem5  19410  volsup  19443  uniiccdif  19463  uniioovol  19464  uniiccvol  19465  uniioombllem2  19468  uniioombllem3a  19469  uniioombllem4  19471  uniioombllem5  19472  mbfimaopnlem  19540  limccnp  19771  dvcobr  19825  dvcjbr  19828  dvfre  19830  evlssca  19936  evl1val  19941  plycjlem  20187  plycj  20188  coecj  20189  radcnvlem2  20323  radcnvlem3  20324  radcnvlt2  20328  pserulm  20331  resinf1o  20431  jensen  20820  ftalem3  20850  dchrinv  21038  dchr2sum  21050  dchrisum0re  21200  ex-co  21739  vafval  22075  smfval  22077  vsfval  22107  imsdval  22171  lnocoi  22251  occllem  22798  hocoi  23260  homco1  23297  counop  23417  homco2  23473  hmopco  23519  nlelchi  23557  kbass2  23613  kbass5  23616  leopsq  23625  hmopidmchi  23647  elpjrn  23686  pjinvari  23687  eflgam  24822  derangenlem  24850  subfacp1lem5  24863  cnpcon  24910  txsconlem  24920  txscon  24921  cvmliftmolem1  24961  cvmliftlem7  24971  cvmlift2lem3  24985  cvmlift2lem7  24989  cvmlift2lem9  24991  cvmliftphtlem  24997  cvmlift3lem1  24999  cvmlift3lem2  25000  cvmlift3lem4  25002  cvmlift3lem5  25003  cvmlift3lem6  25004  cvmlift3lem7  25005  sinccvglem  25102  prodmolem3  25252  fprodf1o  25265  fprodser  25268  fprodcl2lem  25269  fprodmul  25277  fproddiv  25278  fprodn0  25296  iprodefisumlem  25310  iprodefisum  25311  mblfinlem  26235  ftc1anclem5  26275  ftc1anclem8  26278  cocanfo  26411  f1ocan1fv  26420  upixp  26423  ghomco  26550  rngohomco  26582  climexp  27699  stoweidlem27  27744  stoweidlem31  27748  lautco  30832  ldilco  30851  ltrncoval  30880  tendocoval  31501  tendoconid  31564  tendospass  31755  dicvscacl  31927  cdlemn3  31933  cdlemn9  31941
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4323  ax-nul 4331  ax-pow 4370  ax-pr 4396
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2703  df-rex 2704  df-rab 2707  df-v 2951  df-sbc 3155  df-dif 3316  df-un 3318  df-in 3320  df-ss 3327  df-nul 3622  df-if 3733  df-sn 3813  df-pr 3814  df-op 3816  df-uni 4009  df-br 4206  df-opab 4260  df-id 4491  df-xp 4877  df-rel 4878  df-cnv 4879  df-co 4880  df-dm 4881  df-rn 4882  df-res 4883  df-ima 4884  df-iota 5411  df-fun 5449  df-fn 5450  df-f 5451  df-fv 5455
  Copyright terms: Public domain W3C validator