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

Theorem fvco3 6941
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 6669 . 2 (𝐺:𝐴𝐵𝐺 Fn 𝐴)
2 fvco2 6939 . 2 ((𝐺 Fn 𝐴𝐶𝐴) → ((𝐹𝐺)‘𝐶) = (𝐹‘(𝐺𝐶)))
31, 2sylan 581 1 ((𝐺:𝐴𝐵𝐶𝐴) → ((𝐹𝐺)‘𝐶) = (𝐹‘(𝐺𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wcel 2107  ccom 5638   Fn wfn 6492  wf 6493  cfv 6497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-fv 6505
This theorem is referenced by:  fvco3d  6942  foco2  7058  f1cofveqaeqALT  7207  f1ocnvfv1  7223  f1ocnvfv2  7224  fcof1  7234  fcofo  7235  cocan1  7238  cocan2  7239  fveqf1o  7250  isotr  7282  fipreima  9303  fsuppco2  9340  fsuppcor  9341  unxpwdom2  9525  wemapwe  9634  ackbij2lem2  10177  cofsmo  10206  cfcoflem  10209  isf32lem6  10295  isf32lem7  10296  isf32lem8  10297  isf34lem7  10316  isf34lem6  10317  axcc3  10375  axdc4lem  10392  inar1  10712  axdc4uzlem  13889  seqf1olem2  13949  seqf1o  13950  lswco  14729  lo1o1  15415  o1co  15469  caucvgrlem2  15560  summolem3  15600  fsumf1o  15609  fsumcl2lem  15617  fsumadd  15626  fsummulc2  15670  fsumrelem  15693  supcvg  15742  prodmolem3  15817  fprodf1o  15830  fprodser  15833  fprodcl2lem  15834  fprodmul  15844  fproddiv  15845  fprodn0  15863  ruclem11  16123  ruclem12  16124  algcvg  16453  eulerthlem2  16655  cofu1  17771  cofu2  17773  cofucl  17775  fucidcl  17855  fuclid  17856  fucrid  17857  homadm  17927  homacd  17928  evlfcl  18112  curfuncf  18128  yonedalem4c  18167  yonedalem3b  18169  mhmco  18635  prdspjmhm  18640  pwsco1mhm  18643  lactghmga  19188  frgpup3lem  19560  gsumval3eu  19682  gsumval3  19685  gsumzaddlem  19699  gsumzmhm  19715  dprdf1o  19812  gsumfsum  20867  zrhpsgninv  20992  zrhpsgnevpm  20998  zrhpsgnodpm  20999  evlssca  21502  evls1val  21689  evls1sca  21692  evl1val  21698  mdetralt  21960  mdetunilem7  21970  cpmadumatpoly  22235  chcoeffeqlem  22237  cnpco  22621  lmcnp  22658  upxp  22977  uptx  22979  cnmpt11  23017  cnmpt21  23025  xkofvcn  23038  prdstmdd  23478  prdstgpd  23479  comet  23872  prdsxmslem2  23888  nrmmetd  23933  isngp3  23957  ngpds  23963  tngnm  24018  nmoco  24104  cnmetdval  24137  climcncf  24266  cncfco  24273  htpyco1  24344  htpyco2  24345  phtpyco2  24356  reparphti  24363  copco  24384  pi1cof  24425  pi1coghm  24427  caubl  24675  caublcls  24676  cniccbdd  24828  ovolfioo  24834  ovolficc  24835  ovolfsval  24837  ovolicc2lem1  24884  ovolicc2lem4  24887  ovolicc2lem5  24888  volsup  24923  uniiccdif  24945  uniioovol  24946  uniiccvol  24947  uniioombllem2  24950  uniioombllem3a  24951  uniioombllem4  24953  uniioombllem5  24954  mbfimaopnlem  25022  limccnp  25258  dvcobr  25313  dvcjbr  25316  dvfre  25318  plycjlem  25640  plycj  25641  coecj  25642  radcnvlem2  25776  radcnvlem3  25777  radcnvlt2  25781  pserulm  25784  resinf1o  25895  jensen  26341  eflgam  26397  ftalem3  26427  dchrinv  26612  dchr2sum  26624  dchrisum0re  26864  motco  27485  motcgrg  27489  ex-co  29385  vafval  29548  smfval  29550  vsfval  29578  imsdval  29631  lnocoi  29702  occllem  30248  hocoi  30709  homco1  30746  counop  30866  homco2  30922  hmopco  30968  nlelchi  31006  kbass2  31062  kbass5  31065  leopsq  31074  hmopidmchi  31096  elpjrn  31135  pjinvari  31136  cycpmco2  31985  derangenlem  33768  subfacp1lem5  33781  cnpconn  33827  txsconnlem  33837  txsconn  33838  cvmliftmolem1  33878  cvmliftlem7  33888  cvmlift2lem3  33902  cvmlift2lem7  33906  cvmlift2lem9  33908  cvmliftphtlem  33914  cvmlift3lem1  33916  cvmlift3lem2  33917  cvmlift3lem4  33919  cvmlift3lem5  33920  cvmlift3lem6  33921  cvmlift3lem7  33922  mrsubco  34118  msubco  34128  mclsppslem  34180  sinccvglem  34263  iprodefisumlem  34316  iprodefisum  34317  poimirlem22  36103  mblfinlem2  36119  ftc1anclem5  36158  ftc1anclem8  36161  cocanfo  36180  f1ocan1fv  36188  upixp  36191  ghomco  36353  rngohomco  36436  lautco  38563  ldilco  38582  ltrncoval  38611  tendocoval  39232  tendoconid  39295  tendospass  39485  dicvscacl  39657  cdlemn3  39663  cdlemn9  39671  brcoffn  42309  fvovco  43420  climexp  43853  stoweidlem27  44275  stoweidlem31  44279  ovolval4lem1  44897  isomushgr  46025  mgmhmco  46102
  Copyright terms: Public domain W3C validator