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

Theorem fvco3 5634
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 5427 . 2  |-  ( G : A --> B  ->  G  Fn  A )
2 fvco2 5632 . 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 1633    e. wcel 1701    o. ccom 4730    Fn wfn 5287   -->wf 5288   ` cfv 5292
This theorem is referenced by:  foco2  5718  f1ocnvfv1  5834  f1ocnvfv2  5835  fcof1  5839  fcofo  5840  cocan1  5843  cocan2  5844  fveqf1o  5848  isotr  5875  algrflem  6266  fipreima  7206  unxpwdom2  7347  wemapwe  7445  ackbij2lem2  7911  cofsmo  7940  cfcoflem  7943  isf32lem6  8029  isf32lem7  8030  isf32lem8  8031  isf34lem7  8050  isf34lem6  8051  axcc3  8109  axdc4lem  8126  canthp1lem2  8320  inar1  8442  axdc4uzlem  11091  seqf1olem2  11133  seqf1o  11134  lo1o1  12053  o1co  12107  caucvgrlem2  12194  summolem3  12234  fsumf1o  12243  fsumcl2lem  12251  fsumadd  12258  fsummulc2  12293  fsumrelem  12312  supcvg  12361  ruclem11  12565  ruclem12  12566  algcvg  12793  eulerthlem2  12897  cofu1  13807  cofu2  13809  cofucl  13811  fucidcl  13888  fuclid  13889  fucrid  13890  homadm  13921  homacd  13922  evlfcl  14045  curfuncf  14061  yonedalem4c  14100  yonedalem3b  14102  yonedainv  14104  mhmco  14488  prdspjmhm  14492  pwsco1mhm  14495  lactghmga  14833  frgpup3lem  15135  gsumval3eu  15239  gsumval3  15240  gsumzaddlem  15252  gsumzmhm  15259  gsumzinv  15266  gsumsub  15268  dprdf1o  15316  mplsubglem  16228  gsumfsum  16495  frgpcyg  16583  cnpco  17052  lmcnp  17088  upxp  17373  uptx  17375  cnmpt11  17413  cnmpt21  17421  xkofvcn  17434  prdstmdd  17858  prdstgpd  17859  comet  18111  prdsxmslem2  18127  nrmmetd  18149  isngp3  18172  ngpds  18177  tngnm  18219  nmoco  18298  cnmetdval  18332  climcncf  18456  cncfco  18463  htpyco1  18529  htpyco2  18530  phtpyco2  18541  reparphti  18548  copco  18569  pi1cof  18610  pi1coghm  18612  caubl  18786  caublcls  18787  cniccbdd  18874  ovolfioo  18880  ovolficc  18881  ovolfsval  18883  ovolicc2lem1  18929  ovolicc2lem4  18932  ovolicc2lem5  18933  volsup  18966  uniiccdif  18986  uniioovol  18987  uniiccvol  18988  uniioombllem2  18991  uniioombllem3a  18992  uniioombllem4  18994  uniioombllem5  18995  mbfimaopnlem  19063  limccnp  19294  dvcobr  19348  dvcjbr  19351  dvfre  19353  evlssca  19459  evl1val  19464  plycjlem  19710  plycj  19711  coecj  19712  radcnvlem2  19843  radcnvlem3  19844  radcnvlt2  19848  pserulm  19851  resinf1o  19951  jensen  20336  ftalem3  20365  dchrinv  20553  dchr2sum  20565  dchrisum0re  20715  ex-co  20878  vafval  21214  smfval  21216  vsfval  21246  imsdval  21310  lnocoi  21390  occllem  21937  hocoi  22399  homco1  22436  counop  22556  homco2  22612  hmopco  22658  nlelchi  22696  kbass2  22752  kbass5  22755  leopsq  22764  hmopidmchi  22786  elpjrn  22825  pjinvari  22826  derangenlem  23986  subfacp1lem5  23999  cnpcon  24045  txsconlem  24055  txscon  24056  cvmliftmolem1  24096  cvmliftlem7  24106  cvmlift2lem3  24120  cvmlift2lem7  24124  cvmlift2lem9  24126  cvmliftphtlem  24132  cvmlift3lem1  24134  cvmlift3lem2  24135  cvmlift3lem4  24137  cvmlift3lem5  24138  cvmlift3lem6  24139  cvmlift3lem7  24140  sinccvglem  24289  prodmolem3  24436  fprodf1o  24449  fprodser  24452  fprodcl2lem  24453  fprodmul  24461  cocanfo  25523  f1ocan1fv  25543  upixp  25552  ghomco  25721  rngohomco  25753  climexp  26879  stoweidlem27  26924  stoweidlem31  26928  lautco  30104  ldilco  30123  ltrncoval  30152  tendocoval  30773  tendoconid  30836  tendospass  31027  dicvscacl  31199  cdlemn3  31205  cdlemn9  31213
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-sbc 3026  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-opab 4115  df-id 4346  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-fv 5300
  Copyright terms: Public domain W3C validator