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

Theorem fvco3 6438
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 6206 . 2 (𝐺:𝐴𝐵𝐺 Fn 𝐴)
2 fvco2 6436 . 2 ((𝐺 Fn 𝐴𝐶𝐴) → ((𝐹𝐺)‘𝐶) = (𝐹‘(𝐺𝐶)))
31, 2sylan 489 1 ((𝐺:𝐴𝐵𝐶𝐴) → ((𝐹𝐺)‘𝐶) = (𝐹‘(𝐺𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1632  wcel 2139  ccom 5270   Fn wfn 6044  wf 6045  cfv 6049
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-fv 6057
This theorem is referenced by:  foco2  6543  foco2OLD  6544  f1cofveqaeqALT  6680  f1ocnvfv1  6696  f1ocnvfv2  6697  fcof1  6706  fcofo  6707  cocan1  6710  cocan2  6711  fveqf1o  6721  isotr  6750  algrflem  7455  fipreima  8439  fsuppco2  8475  fsuppcor  8476  unxpwdom2  8660  wemapwe  8769  ackbij2lem2  9274  cofsmo  9303  cfcoflem  9306  isf32lem6  9392  isf32lem7  9393  isf32lem8  9394  isf34lem7  9413  isf34lem6  9414  axcc3  9472  axdc4lem  9489  canthp1lem2  9687  inar1  9809  axdc4uzlem  12996  seqf1olem2  13055  seqf1o  13056  lswco  13804  lo1o1  14482  o1co  14536  caucvgrlem2  14624  summolem3  14664  fsumf1o  14673  fsumcl2lem  14681  fsumadd  14689  fsummulc2  14735  fsumrelem  14758  supcvg  14807  prodmolem3  14882  fprodf1o  14895  fprodser  14898  fprodcl2lem  14899  fprodmul  14909  fproddiv  14910  fprodn0  14928  ruclem11  15188  ruclem12  15189  algcvg  15511  eulerthlem2  15709  cofu1  16765  cofu2  16767  cofucl  16769  fucidcl  16846  fuclid  16847  fucrid  16848  homadm  16911  homacd  16912  evlfcl  17083  curfuncf  17099  yonedalem4c  17138  yonedalem3b  17140  yonedainv  17142  mhmco  17583  prdspjmhm  17588  pwsco1mhm  17591  lactghmga  18044  frgpup3lem  18410  gsumval3eu  18525  gsumval3  18528  gsumzaddlem  18541  gsumzmhm  18557  dprdf1o  18651  mplsubglem  19656  evlssca  19744  evls1val  19907  evls1sca  19910  evl1val  19915  gsumfsum  20035  frgpcyg  20144  zrhpsgninv  20153  zrhpsgnevpm  20159  zrhpsgnodpm  20160  mdetralt  20636  mdetunilem7  20646  cpmadumatpoly  20910  chcoeffeqlem  20912  cnpco  21293  lmcnp  21330  upxp  21648  uptx  21650  cnmpt11  21688  cnmpt21  21696  xkofvcn  21709  prdstmdd  22148  prdstgpd  22149  comet  22539  prdsxmslem2  22555  nrmmetd  22600  isngp3  22623  ngpds  22629  tngnm  22676  nmoco  22762  cnmetdval  22795  climcncf  22924  cncfco  22931  htpyco1  22998  htpyco2  22999  phtpyco2  23010  reparphti  23017  copco  23038  pi1cof  23079  pi1coghm  23081  caubl  23326  caublcls  23327  cniccbdd  23450  ovolfioo  23456  ovolficc  23457  ovolfsval  23459  ovolicc2lem1  23505  ovolicc2lem4  23508  ovolicc2lem5  23509  volsup  23544  uniiccdif  23566  uniioovol  23567  uniiccvol  23568  uniioombllem2  23571  uniioombllem3a  23572  uniioombllem4  23574  uniioombllem5  23575  mbfimaopnlem  23641  limccnp  23874  dvcobr  23928  dvcjbr  23931  dvfre  23933  plycjlem  24251  plycj  24252  coecj  24253  radcnvlem2  24387  radcnvlem3  24388  radcnvlt2  24392  pserulm  24395  resinf1o  24502  jensen  24935  eflgam  24991  ftalem3  25021  dchrinv  25206  dchr2sum  25218  dchrisum0re  25422  motco  25655  motcgrg  25659  ex-co  27627  vafval  27788  smfval  27790  vsfval  27818  imsdval  27871  lnocoi  27942  occllem  28492  hocoi  28953  homco1  28990  counop  29110  homco2  29166  hmopco  29212  nlelchi  29250  kbass2  29306  kbass5  29309  leopsq  29318  hmopidmchi  29340  elpjrn  29379  pjinvari  29380  derangenlem  31481  subfacp1lem5  31494  cnpconn  31540  txsconnlem  31550  txsconn  31551  cvmliftmolem1  31591  cvmliftlem7  31601  cvmlift2lem3  31615  cvmlift2lem7  31619  cvmlift2lem9  31621  cvmliftphtlem  31627  cvmlift3lem1  31629  cvmlift3lem2  31630  cvmlift3lem4  31632  cvmlift3lem5  31633  cvmlift3lem6  31634  cvmlift3lem7  31635  mrsubco  31746  msubco  31756  mclsppslem  31808  sinccvglem  31894  iprodefisumlem  31954  iprodefisum  31955  poimirlem22  33762  mblfinlem2  33778  ftc1anclem5  33820  ftc1anclem8  33823  cocanfo  33843  f1ocan1fv  33852  upixp  33855  ghomco  34021  rngohomco  34104  lautco  35904  ldilco  35923  ltrncoval  35952  tendocoval  36574  tendoconid  36637  tendospass  36828  dicvscacl  37000  cdlemn3  37006  cdlemn9  37014  brcoffn  38848  fvco3d  38982  fvovco  39898  climexp  40358  stoweidlem27  40765  stoweidlem31  40769  ovolval4lem1  41387  mgmhmco  42329
  Copyright terms: Public domain W3C validator