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

Theorem fvco3 6468
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 6225 . 2 (𝐺:𝐴𝐵𝐺 Fn 𝐴)
2 fvco2 6466 . 2 ((𝐺 Fn 𝐴𝐶𝐴) → ((𝐹𝐺)‘𝐶) = (𝐹‘(𝐺𝐶)))
31, 2sylan 575 1 ((𝐺:𝐴𝐵𝐶𝐴) → ((𝐹𝐺)‘𝐶) = (𝐹‘(𝐺𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1652  wcel 2155  ccom 5283   Fn wfn 6065  wf 6066  cfv 6070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3599  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-sn 4337  df-pr 4339  df-op 4343  df-uni 4597  df-br 4812  df-opab 4874  df-id 5187  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-fv 6078
This theorem is referenced by:  foco2  6573  f1cofveqaeqALT  6712  f1ocnvfv1  6728  f1ocnvfv2  6729  fcof1  6738  fcofo  6739  cocan1  6742  cocan2  6743  fveqf1o  6753  isotr  6782  algrflem  7492  fipreima  8483  fsuppco2  8519  fsuppcor  8520  unxpwdom2  8704  wemapwe  8813  ackbij2lem2  9319  cofsmo  9348  cfcoflem  9351  isf32lem6  9437  isf32lem7  9438  isf32lem8  9439  isf34lem7  9458  isf34lem6  9459  axcc3  9517  axdc4lem  9534  canthp1lem2  9732  inar1  9854  axdc4uzlem  12997  seqf1olem2  13055  seqf1o  13056  lswco  13884  lo1o1  14564  o1co  14618  caucvgrlem2  14706  summolem3  14746  fsumf1o  14755  fsumcl2lem  14763  fsumadd  14771  fsummulc2  14816  fsumrelem  14839  supcvg  14888  prodmolem3  14962  fprodf1o  14975  fprodser  14978  fprodcl2lem  14979  fprodmul  14989  fproddiv  14990  fprodn0  15008  ruclem11  15267  ruclem12  15268  algcvg  15586  eulerthlem2  15782  cofu1  16825  cofu2  16827  cofucl  16829  fucidcl  16906  fuclid  16907  fucrid  16908  homadm  16971  homacd  16972  evlfcl  17144  curfuncf  17160  yonedalem4c  17199  yonedalem3b  17201  yonedainv  17203  mhmco  17644  prdspjmhm  17649  pwsco1mhm  17652  lactghmga  18103  frgpup3lem  18472  gsumval3eu  18587  gsumval3  18590  gsumzaddlem  18603  gsumzmhm  18619  dprdf1o  18714  mplsubglem  19724  evlssca  19811  evls1val  19974  evls1sca  19977  evl1val  19982  gsumfsum  20102  frgpcyg  20210  zrhpsgninv  20219  zrhpsgnevpm  20225  zrhpsgnodpm  20226  mdetralt  20707  mdetunilem7  20717  cpmadumatpoly  20983  chcoeffeqlem  20985  cnpco  21367  lmcnp  21404  upxp  21722  uptx  21724  cnmpt11  21762  cnmpt21  21770  xkofvcn  21783  prdstmdd  22222  prdstgpd  22223  comet  22613  prdsxmslem2  22629  nrmmetd  22674  isngp3  22697  ngpds  22703  tngnm  22750  nmoco  22836  cnmetdval  22869  climcncf  22998  cncfco  23005  htpyco1  23072  htpyco2  23073  phtpyco2  23084  reparphti  23091  copco  23112  pi1cof  23153  pi1coghm  23155  caubl  23401  caublcls  23402  cniccbdd  23535  ovolfioo  23541  ovolficc  23542  ovolfsval  23544  ovolicc2lem1  23591  ovolicc2lem4  23594  ovolicc2lem5  23595  volsup  23630  uniiccdif  23652  uniioovol  23653  uniiccvol  23654  uniioombllem2  23657  uniioombllem3a  23658  uniioombllem4  23660  uniioombllem5  23661  mbfimaopnlem  23729  limccnp  23962  dvcobr  24016  dvcjbr  24019  dvfre  24021  plycjlem  24339  plycj  24340  coecj  24341  radcnvlem2  24475  radcnvlem3  24476  radcnvlt2  24480  pserulm  24483  resinf1o  24590  jensen  25022  eflgam  25078  ftalem3  25108  dchrinv  25293  dchr2sum  25305  dchrisum0re  25509  motco  25742  motcgrg  25746  ex-co  27777  vafval  27937  smfval  27939  vsfval  27967  imsdval  28020  lnocoi  28091  occllem  28641  hocoi  29102  homco1  29139  counop  29259  homco2  29315  hmopco  29361  nlelchi  29399  kbass2  29455  kbass5  29458  leopsq  29467  hmopidmchi  29489  elpjrn  29528  pjinvari  29529  derangenlem  31624  subfacp1lem5  31637  cnpconn  31683  txsconnlem  31693  txsconn  31694  cvmliftmolem1  31734  cvmliftlem7  31744  cvmlift2lem3  31758  cvmlift2lem7  31762  cvmlift2lem9  31764  cvmliftphtlem  31770  cvmlift3lem1  31772  cvmlift3lem2  31773  cvmlift3lem4  31775  cvmlift3lem5  31776  cvmlift3lem6  31777  cvmlift3lem7  31778  mrsubco  31889  msubco  31899  mclsppslem  31951  sinccvglem  32035  iprodefisumlem  32094  iprodefisum  32095  poimirlem22  33878  mblfinlem2  33894  ftc1anclem5  33935  ftc1anclem8  33938  cocanfo  33958  f1ocan1fv  33967  upixp  33970  ghomco  34135  rngohomco  34218  lautco  36076  ldilco  36095  ltrncoval  36124  tendocoval  36745  tendoconid  36808  tendospass  36998  dicvscacl  37170  cdlemn3  37176  cdlemn9  37184  brcoffn  39028  fvco3d  39162  fvovco  40054  climexp  40501  stoweidlem27  40907  stoweidlem31  40911  ovolval4lem1  41529  mgmhmco  42496
  Copyright terms: Public domain W3C validator