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

Theorem fvco3 5931
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 5717 . 2  |-  ( G : A --> B  ->  G  Fn  A )
2 fvco2 5929 . 2  |-  ( ( G  Fn  A  /\  C  e.  A )  ->  ( ( F  o.  G ) `  C
)  =  ( F `
 ( G `  C ) ) )
31, 2sylan 471 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 369    = wceq 1381    e. wcel 1802    o. ccom 4989    Fn wfn 5569   -->wf 5570   ` cfv 5574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-sbc 3312  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-opab 4492  df-id 4781  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-fv 5582
This theorem is referenced by:  foco2  6032  f1ocnvfv1  6163  f1ocnvfv2  6164  fcof1  6171  fcofo  6172  cocan1  6175  cocan2  6176  fveqf1o  6186  isotr  6213  algrflem  6890  fipreima  7824  fsuppco2  7860  fsuppcor  7861  unxpwdom2  8012  wemapwe  8137  wemapweOLD  8138  ackbij2lem2  8618  cofsmo  8647  cfcoflem  8650  isf32lem6  8736  isf32lem7  8737  isf32lem8  8738  isf34lem7  8757  isf34lem6  8758  axcc3  8816  axdc4lem  8833  canthp1lem2  9029  inar1  9151  axdc4uzlem  12066  seqf1olem2  12121  seqf1o  12122  lswco  12778  lo1o1  13329  o1co  13383  caucvgrlem2  13471  summolem3  13510  fsumf1o  13519  fsumcl2lem  13527  fsumadd  13535  fsummulc2  13573  fsumrelem  13595  supcvg  13641  ruclem11  13845  ruclem12  13846  algcvg  14077  eulerthlem2  14184  cofu1  15122  cofu2  15124  cofucl  15126  fucidcl  15203  fuclid  15204  fucrid  15205  homadm  15236  homacd  15237  evlfcl  15360  curfuncf  15376  yonedalem4c  15415  yonedalem3b  15417  yonedainv  15419  mhmco  15862  prdspjmhm  15867  pwsco1mhm  15870  lactghmga  16298  frgpup3lem  16664  gsumval3eu  16776  gsumval3OLD  16777  gsumval3  16780  gsumzaddlem  16803  gsumzaddlemOLD  16805  gsumzmhm  16826  gsumzmhmOLD  16827  gsumzinvOLD  16839  gsumsubOLD  16844  dprdf1o  16947  mplsubglem  17961  mplsubglemOLD  17963  evlssca  18059  evls1val  18225  evls1sca  18228  evl1val  18233  gsumfsum  18352  frgpcyg  18479  zrhpsgninv  18488  zrhpsgnevpm  18494  zrhpsgnodpm  18495  mdetralt  18977  mdetunilem7  18987  cpmadumatpoly  19251  chcoeffeqlem  19253  cnpco  19634  lmcnp  19671  upxp  19990  uptx  19992  cnmpt11  20030  cnmpt21  20038  xkofvcn  20051  prdstmdd  20488  prdstgpd  20489  comet  20882  prdsxmslem2  20898  nrmmetd  20961  isngp3  20984  ngpds  20989  tngnm  21031  nmoco  21110  cnmetdval  21144  climcncf  21270  cncfco  21277  htpyco1  21344  htpyco2  21345  phtpyco2  21356  reparphti  21363  copco  21384  pi1cof  21425  pi1coghm  21427  caubl  21612  caublcls  21613  cniccbdd  21739  ovolfioo  21745  ovolficc  21746  ovolfsval  21748  ovolicc2lem1  21794  ovolicc2lem4  21797  ovolicc2lem5  21798  volsup  21832  uniiccdif  21853  uniioovol  21854  uniiccvol  21855  uniioombllem2  21858  uniioombllem3a  21859  uniioombllem4  21861  uniioombllem5  21862  mbfimaopnlem  21928  limccnp  22161  dvcobr  22215  dvcjbr  22218  dvfre  22220  plycjlem  22538  plycj  22539  coecj  22540  radcnvlem2  22674  radcnvlem3  22675  radcnvlt2  22679  pserulm  22682  resinf1o  22788  jensen  23183  ftalem3  23213  dchrinv  23401  dchr2sum  23413  dchrisum0re  23563  motco  23792  motcgrg  23796  ex-co  25024  vafval  25361  smfval  25363  vsfval  25393  imsdval  25457  lnocoi  25537  occllem  26086  hocoi  26548  homco1  26585  counop  26705  homco2  26761  hmopco  26807  nlelchi  26845  kbass2  26901  kbass5  26904  leopsq  26913  hmopidmchi  26935  elpjrn  26974  pjinvari  26975  eflgam  28453  derangenlem  28481  subfacp1lem5  28494  cnpcon  28541  txsconlem  28551  txscon  28552  cvmliftmolem1  28592  cvmliftlem7  28602  cvmlift2lem3  28616  cvmlift2lem7  28620  cvmlift2lem9  28622  cvmliftphtlem  28628  cvmlift3lem1  28630  cvmlift3lem2  28631  cvmlift3lem4  28633  cvmlift3lem5  28634  cvmlift3lem6  28635  cvmlift3lem7  28636  mrsubco  28747  msubco  28757  mclsppslem  28809  sinccvglem  28904  prodmolem3  29033  fprodf1o  29046  fprodser  29049  fprodcl2lem  29050  fprodmul  29058  fproddiv  29059  fprodn0  29077  iprodefisumlem  29091  iprodefisum  29092  mblfinlem2  30020  ftc1anclem5  30062  ftc1anclem8  30065  cocanfo  30176  f1ocan1fv  30185  upixp  30188  ghomco  30313  rngohomco  30345  climexp  31515  stoweidlem27  31694  stoweidlem31  31698  mgmhmco  32323  lautco  35523  ldilco  35542  ltrncoval  35571  tendocoval  36194  tendoconid  36257  tendospass  36448  dicvscacl  36620  cdlemn3  36626  cdlemn9  36634  fvco3d  37583
  Copyright terms: Public domain W3C validator