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

Theorem fvco3 6753
Description: Value of a function composition. (Contributed by NM, 3-Jan-2004.) (Revised by Mario Carneiro, 26-Dec-2014.)
Assertion
Ref Expression
fvco3 ((𝐺:𝐴𝐵𝐶𝐴) → ((𝐹𝐺)‘𝐶) = (𝐹‘(𝐺𝐶)))

Proof of Theorem fvco3
StepHypRef Expression
1 ffn 6507 . 2 (𝐺:𝐴𝐵𝐺 Fn 𝐴)
2 fvco2 6751 . 2 ((𝐺 Fn 𝐴𝐶𝐴) → ((𝐹𝐺)‘𝐶) = (𝐹‘(𝐺𝐶)))
31, 2sylan 580 1 ((𝐺:𝐴𝐵𝐶𝐴) → ((𝐹𝐺)‘𝐶) = (𝐹‘(𝐺𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  wcel 2105  ccom 5552   Fn wfn 6343  wf 6344  cfv 6348
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-fv 6356
This theorem is referenced by:  fvco3d  6754  foco2  6865  f1cofveqaeqALT  7008  f1ocnvfv1  7024  f1ocnvfv2  7025  fcof1  7034  fcofo  7035  cocan1  7038  cocan2  7039  fveqf1o  7049  isotr  7078  algrflem  7808  fipreima  8818  fsuppco2  8854  fsuppcor  8855  unxpwdom2  9040  wemapwe  9148  ackbij2lem2  9650  cofsmo  9679  cfcoflem  9682  isf32lem6  9768  isf32lem7  9769  isf32lem8  9770  isf34lem7  9789  isf34lem6  9790  axcc3  9848  axdc4lem  9865  canthp1lem2  10063  inar1  10185  axdc4uzlem  13339  seqf1olem2  13398  seqf1o  13399  lswco  14189  lo1o1  14877  o1co  14931  caucvgrlem2  15019  summolem3  15059  fsumf1o  15068  fsumcl2lem  15076  fsumadd  15084  fsummulc2  15127  fsumrelem  15150  supcvg  15199  prodmolem3  15275  fprodf1o  15288  fprodser  15291  fprodcl2lem  15292  fprodmul  15302  fproddiv  15303  fprodn0  15321  ruclem11  15581  ruclem12  15582  algcvg  15908  eulerthlem2  16107  cofu1  17142  cofu2  17144  cofucl  17146  fucidcl  17223  fuclid  17224  fucrid  17225  homadm  17288  homacd  17289  evlfcl  17460  curfuncf  17476  yonedalem4c  17515  yonedalem3b  17517  mhmco  17976  prdspjmhm  17981  pwsco1mhm  17984  lactghmga  18462  frgpup3lem  18832  gsumval3eu  18953  gsumval3  18956  gsumzaddlem  18970  gsumzmhm  18986  dprdf1o  19083  mplsubglem  20142  evlssca  20230  evls1val  20411  evls1sca  20414  evl1val  20420  gsumfsum  20540  zrhpsgninv  20657  zrhpsgnevpm  20663  zrhpsgnodpm  20664  mdetralt  21145  mdetunilem7  21155  cpmadumatpoly  21419  chcoeffeqlem  21421  cnpco  21803  lmcnp  21840  upxp  22159  uptx  22161  cnmpt11  22199  cnmpt21  22207  xkofvcn  22220  prdstmdd  22659  prdstgpd  22660  comet  23050  prdsxmslem2  23066  nrmmetd  23111  isngp3  23134  ngpds  23140  tngnm  23187  nmoco  23273  cnmetdval  23306  climcncf  23435  cncfco  23442  htpyco1  23509  htpyco2  23510  phtpyco2  23521  reparphti  23528  copco  23549  pi1cof  23590  pi1coghm  23592  caubl  23838  caublcls  23839  cniccbdd  23989  ovolfioo  23995  ovolficc  23996  ovolfsval  23998  ovolicc2lem1  24045  ovolicc2lem4  24048  ovolicc2lem5  24049  volsup  24084  uniiccdif  24106  uniioovol  24107  uniiccvol  24108  uniioombllem2  24111  uniioombllem3a  24112  uniioombllem4  24114  uniioombllem5  24115  mbfimaopnlem  24183  limccnp  24416  dvcobr  24470  dvcjbr  24473  dvfre  24475  plycjlem  24793  plycj  24794  coecj  24795  radcnvlem2  24929  radcnvlem3  24930  radcnvlt2  24934  pserulm  24937  resinf1o  25047  jensen  25493  eflgam  25549  ftalem3  25579  dchrinv  25764  dchr2sum  25776  dchrisum0re  26016  motco  26253  motcgrg  26257  ex-co  28144  vafval  28307  smfval  28309  vsfval  28337  imsdval  28390  lnocoi  28461  occllem  29007  hocoi  29468  homco1  29505  counop  29625  homco2  29681  hmopco  29727  nlelchi  29765  kbass2  29821  kbass5  29824  leopsq  29833  hmopidmchi  29855  elpjrn  29894  pjinvari  29895  cycpmco2  30702  derangenlem  32315  subfacp1lem5  32328  cnpconn  32374  txsconnlem  32384  txsconn  32385  cvmliftmolem1  32425  cvmliftlem7  32435  cvmlift2lem3  32449  cvmlift2lem7  32453  cvmlift2lem9  32455  cvmliftphtlem  32461  cvmlift3lem1  32463  cvmlift3lem2  32464  cvmlift3lem4  32466  cvmlift3lem5  32467  cvmlift3lem6  32468  cvmlift3lem7  32469  mrsubco  32665  msubco  32675  mclsppslem  32727  sinccvglem  32812  iprodefisumlem  32869  iprodefisum  32870  poimirlem22  34795  mblfinlem2  34811  ftc1anclem5  34852  ftc1anclem8  34855  cocanfo  34874  f1ocan1fv  34882  upixp  34885  ghomco  35050  rngohomco  35133  lautco  37113  ldilco  37132  ltrncoval  37161  tendocoval  37782  tendoconid  37845  tendospass  38035  dicvscacl  38207  cdlemn3  38213  cdlemn9  38221  brcoffn  40258  fvovco  41331  climexp  41762  stoweidlem27  42189  stoweidlem31  42193  ovolval4lem1  42808  isomushgr  43868  mgmhmco  43945
  Copyright terms: Public domain W3C validator