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

Theorem fvco3 6314
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 6083 . 2 (𝐺:𝐴𝐵𝐺 Fn 𝐴)
2 fvco2 6312 . 2 ((𝐺 Fn 𝐴𝐶𝐴) → ((𝐹𝐺)‘𝐶) = (𝐹‘(𝐺𝐶)))
31, 2sylan 487 1 ((𝐺:𝐴𝐵𝐶𝐴) → ((𝐹𝐺)‘𝐶) = (𝐹‘(𝐺𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1523  wcel 2030  ccom 5147   Fn wfn 5921  wf 5922  cfv 5926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-fv 5934
This theorem is referenced by:  foco2  6419  foco2OLD  6420  f1cofveqaeqALT  6556  f1ocnvfv1  6572  f1ocnvfv2  6573  fcof1  6582  fcofo  6583  cocan1  6586  cocan2  6587  fveqf1o  6597  isotr  6626  algrflem  7331  fipreima  8313  fsuppco2  8349  fsuppcor  8350  unxpwdom2  8534  wemapwe  8632  ackbij2lem2  9100  cofsmo  9129  cfcoflem  9132  isf32lem6  9218  isf32lem7  9219  isf32lem8  9220  isf34lem7  9239  isf34lem6  9240  axcc3  9298  axdc4lem  9315  canthp1lem2  9513  inar1  9635  axdc4uzlem  12822  seqf1olem2  12881  seqf1o  12882  lswco  13630  lo1o1  14307  o1co  14361  caucvgrlem2  14449  summolem3  14489  fsumf1o  14498  fsumcl2lem  14506  fsumadd  14514  fsummulc2  14560  fsumrelem  14583  supcvg  14632  prodmolem3  14707  fprodf1o  14720  fprodser  14723  fprodcl2lem  14724  fprodmul  14734  fproddiv  14735  fprodn0  14753  ruclem11  15013  ruclem12  15014  algcvg  15336  eulerthlem2  15534  cofu1  16591  cofu2  16593  cofucl  16595  fucidcl  16672  fuclid  16673  fucrid  16674  homadm  16737  homacd  16738  evlfcl  16909  curfuncf  16925  yonedalem4c  16964  yonedalem3b  16966  yonedainv  16968  mhmco  17409  prdspjmhm  17414  pwsco1mhm  17417  lactghmga  17870  frgpup3lem  18236  gsumval3eu  18351  gsumval3  18354  gsumzaddlem  18367  gsumzmhm  18383  dprdf1o  18477  mplsubglem  19482  evlssca  19570  evls1val  19733  evls1sca  19736  evl1val  19741  gsumfsum  19861  frgpcyg  19970  zrhpsgninv  19979  zrhpsgnevpm  19985  zrhpsgnodpm  19986  mdetralt  20462  mdetunilem7  20472  cpmadumatpoly  20736  chcoeffeqlem  20738  cnpco  21119  lmcnp  21156  upxp  21474  uptx  21476  cnmpt11  21514  cnmpt21  21522  xkofvcn  21535  prdstmdd  21974  prdstgpd  21975  comet  22365  prdsxmslem2  22381  nrmmetd  22426  isngp3  22449  ngpds  22455  tngnm  22502  nmoco  22588  cnmetdval  22621  climcncf  22750  cncfco  22757  htpyco1  22824  htpyco2  22825  phtpyco2  22836  reparphti  22843  copco  22864  pi1cof  22905  pi1coghm  22907  caubl  23152  caublcls  23153  cniccbdd  23276  ovolfioo  23282  ovolficc  23283  ovolfsval  23285  ovolicc2lem1  23331  ovolicc2lem4  23334  ovolicc2lem5  23335  volsup  23370  uniiccdif  23392  uniioovol  23393  uniiccvol  23394  uniioombllem2  23397  uniioombllem3a  23398  uniioombllem4  23400  uniioombllem5  23401  mbfimaopnlem  23467  limccnp  23700  dvcobr  23754  dvcjbr  23757  dvfre  23759  plycjlem  24077  plycj  24078  coecj  24079  radcnvlem2  24213  radcnvlem3  24214  radcnvlt2  24218  pserulm  24221  resinf1o  24327  jensen  24760  eflgam  24816  ftalem3  24846  dchrinv  25031  dchr2sum  25043  dchrisum0re  25247  motco  25480  motcgrg  25484  ex-co  27425  vafval  27586  smfval  27588  vsfval  27616  imsdval  27669  lnocoi  27740  occllem  28290  hocoi  28751  homco1  28788  counop  28908  homco2  28964  hmopco  29010  nlelchi  29048  kbass2  29104  kbass5  29107  leopsq  29116  hmopidmchi  29138  elpjrn  29177  pjinvari  29178  derangenlem  31279  subfacp1lem5  31292  cnpconn  31338  txsconnlem  31348  txsconn  31349  cvmliftmolem1  31389  cvmliftlem7  31399  cvmlift2lem3  31413  cvmlift2lem7  31417  cvmlift2lem9  31419  cvmliftphtlem  31425  cvmlift3lem1  31427  cvmlift3lem2  31428  cvmlift3lem4  31430  cvmlift3lem5  31431  cvmlift3lem6  31432  cvmlift3lem7  31433  mrsubco  31544  msubco  31554  mclsppslem  31606  sinccvglem  31692  iprodefisumlem  31752  iprodefisum  31753  poimirlem22  33561  mblfinlem2  33577  ftc1anclem5  33619  ftc1anclem8  33622  cocanfo  33642  f1ocan1fv  33651  upixp  33654  ghomco  33820  rngohomco  33903  lautco  35701  ldilco  35720  ltrncoval  35749  tendocoval  36371  tendoconid  36434  tendospass  36625  dicvscacl  36797  cdlemn3  36803  cdlemn9  36811  brcoffn  38645  fvco3d  38779  fvovco  39695  climexp  40155  stoweidlem27  40562  stoweidlem31  40566  ovolval4lem1  41184  mgmhmco  42126
  Copyright terms: Public domain W3C validator