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

Theorem fvco3 5756
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 5547 . 2  |-  ( G : A --> B  ->  G  Fn  A )
2 fvco2 5754 . 2  |-  ( ( G  Fn  A  /\  C  e.  A )  ->  ( ( F  o.  G ) `  C
)  =  ( F `
 ( G `  C ) ) )
31, 2sylan 468 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 1362    e. wcel 1755    o. ccom 4831    Fn wfn 5401   -->wf 5402   ` cfv 5406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-fv 5414
This theorem is referenced by:  foco2  5851  f1ocnvfv1  5970  f1ocnvfv2  5971  fcof1  5978  fcofo  5979  cocan1  5982  cocan2  5983  fveqf1o  5987  isotr  6014  algrflem  6670  fipreima  7605  fsuppco2  7640  fsuppcor  7641  unxpwdom2  7791  wemapwe  7916  wemapweOLD  7917  ackbij2lem2  8397  cofsmo  8426  cfcoflem  8429  isf32lem6  8515  isf32lem7  8516  isf32lem8  8517  isf34lem7  8536  isf34lem6  8537  axcc3  8595  axdc4lem  8612  canthp1lem2  8807  inar1  8929  axdc4uzlem  11787  seqf1olem2  11829  seqf1o  11830  lswco  12449  lo1o1  12993  o1co  13047  caucvgrlem2  13135  summolem3  13174  fsumf1o  13183  fsumcl2lem  13191  fsumadd  13198  fsummulc2  13233  fsumrelem  13252  supcvg  13300  ruclem11  13504  ruclem12  13505  algcvg  13733  eulerthlem2  13839  cofu1  14776  cofu2  14778  cofucl  14780  fucidcl  14857  fuclid  14858  fucrid  14859  homadm  14890  homacd  14891  evlfcl  15014  curfuncf  15030  yonedalem4c  15069  yonedalem3b  15071  yonedainv  15073  mhmco  15471  prdspjmhm  15476  pwsco1mhm  15479  lactghmga  15888  frgpup3lem  16253  gsumval3eu  16360  gsumval3OLD  16361  gsumval3  16364  gsumzaddlem  16387  gsumzaddlemOLD  16389  gsumzmhm  16406  gsumzmhmOLD  16407  gsumzinvOLD  16418  gsumsubOLD  16423  dprdf1o  16502  mplsubglem  17443  mplsubglemOLD  17445  gsumfsum  17722  frgpcyg  17847  zrhpsgninv  17856  zrhpsgnevpm  17862  zrhpsgnodpm  17863  mdetralt  18255  mdetunilem7  18265  cnpco  18712  lmcnp  18749  upxp  19037  uptx  19039  cnmpt11  19077  cnmpt21  19085  xkofvcn  19098  prdstmdd  19535  prdstgpd  19536  comet  19929  prdsxmslem2  19945  nrmmetd  20008  isngp3  20031  ngpds  20036  tngnm  20078  nmoco  20157  cnmetdval  20191  climcncf  20317  cncfco  20324  htpyco1  20391  htpyco2  20392  phtpyco2  20403  reparphti  20410  copco  20431  pi1cof  20472  pi1coghm  20474  caubl  20659  caublcls  20660  cniccbdd  20786  ovolfioo  20792  ovolficc  20793  ovolfsval  20795  ovolicc2lem1  20841  ovolicc2lem4  20844  ovolicc2lem5  20845  volsup  20878  uniiccdif  20899  uniioovol  20900  uniiccvol  20901  uniioombllem2  20904  uniioombllem3a  20905  uniioombllem4  20907  uniioombllem5  20908  mbfimaopnlem  20974  limccnp  21207  dvcobr  21261  dvcjbr  21264  dvfre  21266  evlssca  21373  evl1val  21378  plycjlem  21627  plycj  21628  coecj  21629  radcnvlem2  21763  radcnvlem3  21764  radcnvlt2  21768  pserulm  21771  resinf1o  21876  jensen  22266  ftalem3  22296  dchrinv  22484  dchr2sum  22496  dchrisum0re  22646  ex-co  23467  vafval  23803  smfval  23805  vsfval  23835  imsdval  23899  lnocoi  23979  occllem  24528  hocoi  24990  homco1  25027  counop  25147  homco2  25203  hmopco  25249  nlelchi  25287  kbass2  25343  kbass5  25346  leopsq  25355  hmopidmchi  25377  elpjrn  25416  pjinvari  25417  eflgam  26878  derangenlem  26906  subfacp1lem5  26919  cnpcon  26966  txsconlem  26976  txscon  26977  cvmliftmolem1  27017  cvmliftlem7  27027  cvmlift2lem3  27041  cvmlift2lem7  27045  cvmlift2lem9  27047  cvmliftphtlem  27053  cvmlift3lem1  27055  cvmlift3lem2  27056  cvmlift3lem4  27058  cvmlift3lem5  27059  cvmlift3lem6  27060  cvmlift3lem7  27061  sinccvglem  27163  prodmolem3  27292  fprodf1o  27305  fprodser  27308  fprodcl2lem  27309  fprodmul  27317  fproddiv  27318  fprodn0  27336  iprodefisumlem  27350  iprodefisum  27351  mblfinlem2  28270  ftc1anclem5  28312  ftc1anclem8  28315  cocanfo  28452  f1ocan1fv  28461  upixp  28464  ghomco  28589  rngohomco  28621  climexp  29621  stoweidlem27  29665  stoweidlem31  29669  lautco  33311  ldilco  33330  ltrncoval  33359  tendocoval  33980  tendoconid  34043  tendospass  34234  dicvscacl  34406  cdlemn3  34412  cdlemn9  34420
  Copyright terms: Public domain W3C validator