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

Theorem fvco3 5763
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 5554 . 2  |-  ( G : A --> B  ->  G  Fn  A )
2 fvco2 5761 . 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 1369    e. wcel 1756    o. ccom 4839    Fn wfn 5408   -->wf 5409   ` cfv 5413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-fv 5421
This theorem is referenced by:  foco2  5858  f1ocnvfv1  5978  f1ocnvfv2  5979  fcof1  5986  fcofo  5987  cocan1  5990  cocan2  5991  fveqf1o  5995  isotr  6022  algrflem  6676  fipreima  7609  fsuppco2  7644  fsuppcor  7645  unxpwdom2  7795  wemapwe  7920  wemapweOLD  7921  ackbij2lem2  8401  cofsmo  8430  cfcoflem  8433  isf32lem6  8519  isf32lem7  8520  isf32lem8  8521  isf34lem7  8540  isf34lem6  8541  axcc3  8599  axdc4lem  8616  canthp1lem2  8812  inar1  8934  axdc4uzlem  11796  seqf1olem2  11838  seqf1o  11839  lswco  12458  lo1o1  13002  o1co  13056  caucvgrlem2  13144  summolem3  13183  fsumf1o  13192  fsumcl2lem  13200  fsumadd  13207  fsummulc2  13243  fsumrelem  13262  supcvg  13310  ruclem11  13514  ruclem12  13515  algcvg  13743  eulerthlem2  13849  cofu1  14786  cofu2  14788  cofucl  14790  fucidcl  14867  fuclid  14868  fucrid  14869  homadm  14900  homacd  14901  evlfcl  15024  curfuncf  15040  yonedalem4c  15079  yonedalem3b  15081  yonedainv  15083  mhmco  15481  prdspjmhm  15486  pwsco1mhm  15489  lactghmga  15900  frgpup3lem  16265  gsumval3eu  16372  gsumval3OLD  16373  gsumval3  16376  gsumzaddlem  16399  gsumzaddlemOLD  16401  gsumzmhm  16420  gsumzmhmOLD  16421  gsumzinvOLD  16433  gsumsubOLD  16438  dprdf1o  16519  mplsubglem  17490  mplsubglemOLD  17492  evlssca  17588  evls1val  17735  evls1sca  17738  evl1val  17743  gsumfsum  17859  frgpcyg  17986  zrhpsgninv  17995  zrhpsgnevpm  18001  zrhpsgnodpm  18002  mdetralt  18394  mdetunilem7  18404  cnpco  18851  lmcnp  18888  upxp  19176  uptx  19178  cnmpt11  19216  cnmpt21  19224  xkofvcn  19237  prdstmdd  19674  prdstgpd  19675  comet  20068  prdsxmslem2  20084  nrmmetd  20147  isngp3  20170  ngpds  20175  tngnm  20217  nmoco  20296  cnmetdval  20330  climcncf  20456  cncfco  20463  htpyco1  20530  htpyco2  20531  phtpyco2  20542  reparphti  20549  copco  20570  pi1cof  20611  pi1coghm  20613  caubl  20798  caublcls  20799  cniccbdd  20925  ovolfioo  20931  ovolficc  20932  ovolfsval  20934  ovolicc2lem1  20980  ovolicc2lem4  20983  ovolicc2lem5  20984  volsup  21017  uniiccdif  21038  uniioovol  21039  uniiccvol  21040  uniioombllem2  21043  uniioombllem3a  21044  uniioombllem4  21046  uniioombllem5  21047  mbfimaopnlem  21113  limccnp  21346  dvcobr  21400  dvcjbr  21403  dvfre  21405  plycjlem  21723  plycj  21724  coecj  21725  radcnvlem2  21859  radcnvlem3  21860  radcnvlt2  21864  pserulm  21867  resinf1o  21972  jensen  22362  ftalem3  22392  dchrinv  22580  dchr2sum  22592  dchrisum0re  22742  ex-co  23613  vafval  23949  smfval  23951  vsfval  23981  imsdval  24045  lnocoi  24125  occllem  24674  hocoi  25136  homco1  25173  counop  25293  homco2  25349  hmopco  25395  nlelchi  25433  kbass2  25489  kbass5  25492  leopsq  25501  hmopidmchi  25523  elpjrn  25562  pjinvari  25563  eflgam  27000  derangenlem  27028  subfacp1lem5  27041  cnpcon  27088  txsconlem  27098  txscon  27099  cvmliftmolem1  27139  cvmliftlem7  27149  cvmlift2lem3  27163  cvmlift2lem7  27167  cvmlift2lem9  27169  cvmliftphtlem  27175  cvmlift3lem1  27177  cvmlift3lem2  27178  cvmlift3lem4  27180  cvmlift3lem5  27181  cvmlift3lem6  27182  cvmlift3lem7  27183  sinccvglem  27286  prodmolem3  27415  fprodf1o  27428  fprodser  27431  fprodcl2lem  27432  fprodmul  27440  fproddiv  27441  fprodn0  27459  iprodefisumlem  27473  iprodefisum  27474  mblfinlem2  28400  ftc1anclem5  28442  ftc1anclem8  28445  cocanfo  28582  f1ocan1fv  28591  upixp  28594  ghomco  28719  rngohomco  28751  climexp  29749  stoweidlem27  29793  stoweidlem31  29797  lautco  33634  ldilco  33653  ltrncoval  33682  tendocoval  34303  tendoconid  34366  tendospass  34557  dicvscacl  34729  cdlemn3  34735  cdlemn9  34743
  Copyright terms: Public domain W3C validator