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

Theorem fvco3 6232
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 6002 . 2 (𝐺:𝐴𝐵𝐺 Fn 𝐴)
2 fvco2 6230 . 2 ((𝐺 Fn 𝐴𝐶𝐴) → ((𝐹𝐺)‘𝐶) = (𝐹‘(𝐺𝐶)))
31, 2sylan 488 1 ((𝐺:𝐴𝐵𝐶𝐴) → ((𝐹𝐺)‘𝐶) = (𝐹‘(𝐺𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480  wcel 1987  ccom 5078   Fn wfn 5842  wf 5843  cfv 5847
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-fv 5855
This theorem is referenced by:  foco2  6335  foco2OLD  6336  f1cofveqaeqALT  6470  f1ocnvfv1  6486  f1ocnvfv2  6487  fcof1  6496  fcofo  6497  cocan1  6500  cocan2  6501  fveqf1o  6511  isotr  6540  algrflem  7231  fipreima  8216  fsuppco2  8252  fsuppcor  8253  unxpwdom2  8437  wemapwe  8538  ackbij2lem2  9006  cofsmo  9035  cfcoflem  9038  isf32lem6  9124  isf32lem7  9125  isf32lem8  9126  isf34lem7  9145  isf34lem6  9146  axcc3  9204  axdc4lem  9221  canthp1lem2  9419  inar1  9541  axdc4uzlem  12722  seqf1olem2  12781  seqf1o  12782  lswco  13521  lo1o1  14197  o1co  14251  caucvgrlem2  14339  summolem3  14378  fsumf1o  14387  fsumcl2lem  14395  fsumadd  14403  fsummulc2  14444  fsumrelem  14466  supcvg  14513  prodmolem3  14588  fprodf1o  14601  fprodser  14604  fprodcl2lem  14605  fprodmul  14615  fproddiv  14616  fprodn0  14634  ruclem11  14894  ruclem12  14895  algcvg  15213  eulerthlem2  15411  cofu1  16465  cofu2  16467  cofucl  16469  fucidcl  16546  fuclid  16547  fucrid  16548  homadm  16611  homacd  16612  evlfcl  16783  curfuncf  16799  yonedalem4c  16838  yonedalem3b  16840  yonedainv  16842  mhmco  17283  prdspjmhm  17288  pwsco1mhm  17291  lactghmga  17745  frgpup3lem  18111  gsumval3eu  18226  gsumval3  18229  gsumzaddlem  18242  gsumzmhm  18258  dprdf1o  18352  mplsubglem  19353  evlssca  19441  evls1val  19604  evls1sca  19607  evl1val  19612  gsumfsum  19732  frgpcyg  19841  zrhpsgninv  19850  zrhpsgnevpm  19856  zrhpsgnodpm  19857  mdetralt  20333  mdetunilem7  20343  cpmadumatpoly  20607  chcoeffeqlem  20609  cnpco  20981  lmcnp  21018  upxp  21336  uptx  21338  cnmpt11  21376  cnmpt21  21384  xkofvcn  21397  prdstmdd  21837  prdstgpd  21838  comet  22228  prdsxmslem2  22244  nrmmetd  22289  isngp3  22312  ngpds  22318  tngnm  22365  nmoco  22451  cnmetdval  22484  climcncf  22611  cncfco  22618  htpyco1  22685  htpyco2  22686  phtpyco2  22697  reparphti  22705  copco  22726  pi1cof  22767  pi1coghm  22769  caubl  23014  caublcls  23015  cniccbdd  23137  ovolfioo  23143  ovolficc  23144  ovolfsval  23146  ovolicc2lem1  23192  ovolicc2lem4  23195  ovolicc2lem5  23196  volsup  23231  uniiccdif  23252  uniioovol  23253  uniiccvol  23254  uniioombllem2  23257  uniioombllem3a  23258  uniioombllem4  23260  uniioombllem5  23261  mbfimaopnlem  23328  limccnp  23561  dvcobr  23615  dvcjbr  23618  dvfre  23620  plycjlem  23936  plycj  23937  coecj  23938  radcnvlem2  24072  radcnvlem3  24073  radcnvlt2  24077  pserulm  24080  resinf1o  24186  jensen  24615  eflgam  24671  ftalem3  24701  dchrinv  24886  dchr2sum  24898  dchrisum0re  25102  motco  25335  motcgrg  25339  ex-co  27149  vafval  27307  smfval  27309  vsfval  27337  imsdval  27390  lnocoi  27461  occllem  28011  hocoi  28472  homco1  28509  counop  28629  homco2  28685  hmopco  28731  nlelchi  28769  kbass2  28825  kbass5  28828  leopsq  28837  hmopidmchi  28859  elpjrn  28898  pjinvari  28899  derangenlem  30861  subfacp1lem5  30874  cnpconn  30920  txsconnlem  30930  txsconn  30931  cvmliftmolem1  30971  cvmliftlem7  30981  cvmlift2lem3  30995  cvmlift2lem7  30999  cvmlift2lem9  31001  cvmliftphtlem  31007  cvmlift3lem1  31009  cvmlift3lem2  31010  cvmlift3lem4  31012  cvmlift3lem5  31013  cvmlift3lem6  31014  cvmlift3lem7  31015  mrsubco  31126  msubco  31136  mclsppslem  31188  sinccvglem  31274  iprodefisumlem  31334  iprodefisum  31335  poimirlem22  33063  mblfinlem2  33079  ftc1anclem5  33121  ftc1anclem8  33124  cocanfo  33144  f1ocan1fv  33153  upixp  33156  ghomco  33322  rngohomco  33405  lautco  34863  ldilco  34882  ltrncoval  34911  tendocoval  35534  tendoconid  35597  tendospass  35788  dicvscacl  35960  cdlemn3  35966  cdlemn9  35974  brcoffn  37810  fvco3d  37944  fvovco  38855  climexp  39241  stoweidlem27  39551  stoweidlem31  39555  ovolval4lem1  40170  mgmhmco  41089
  Copyright terms: Public domain W3C validator