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

Theorem fvco3 5942
Description: Value of a function composition. (Contributed by NM, 3-Jan-2004.) (Revised by Mario Carneiro, 26-Dec-2014.)
Assertion
Ref Expression
fvco3  |-  ( ( G : A --> B  /\  C  e.  A )  ->  ( ( F  o.  G ) `  C
)  =  ( F `
 ( G `  C ) ) )

Proof of Theorem fvco3
StepHypRef Expression
1 ffn 5728 . 2  |-  ( G : A --> B  ->  G  Fn  A )
2 fvco2 5940 . 2  |-  ( ( G  Fn  A  /\  C  e.  A )  ->  ( ( F  o.  G ) `  C
)  =  ( F `
 ( G `  C ) ) )
31, 2sylan 474 1  |-  ( ( G : A --> B  /\  C  e.  A )  ->  ( ( F  o.  G ) `  C
)  =  ( F `
 ( G `  C ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    = wceq 1444    e. wcel 1887    o. ccom 4838    Fn wfn 5577   -->wf 5578   ` cfv 5582
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-fv 5590
This theorem is referenced by:  foco2  6042  f1ocnvfv1  6175  f1ocnvfv2  6176  fcof1  6185  fcofo  6186  cocan1  6189  cocan2  6190  fveqf1o  6200  isotr  6227  algrflem  6905  fipreima  7880  fsuppco2  7916  fsuppcor  7917  unxpwdom2  8103  wemapwe  8202  ackbij2lem2  8670  cofsmo  8699  cfcoflem  8702  isf32lem6  8788  isf32lem7  8789  isf32lem8  8790  isf34lem7  8809  isf34lem6  8810  axcc3  8868  axdc4lem  8885  canthp1lem2  9078  inar1  9200  axdc4uzlem  12195  seqf1olem2  12253  seqf1o  12254  lswco  12935  lo1o1  13596  o1co  13650  caucvgrlem2  13740  summolem3  13780  fsumf1o  13789  fsumcl2lem  13797  fsumadd  13805  fsummulc2  13845  fsumrelem  13867  supcvg  13914  prodmolem3  13987  fprodf1o  14000  fprodser  14003  fprodcl2lem  14004  fprodmul  14014  fproddiv  14015  fprodn0  14033  ruclem11  14292  ruclem12  14293  algcvg  14535  eulerthlem2  14730  cofu1  15789  cofu2  15791  cofucl  15793  fucidcl  15870  fuclid  15871  fucrid  15872  homadm  15935  homacd  15936  evlfcl  16107  curfuncf  16123  yonedalem4c  16162  yonedalem3b  16164  yonedainv  16166  mhmco  16609  prdspjmhm  16614  pwsco1mhm  16617  lactghmga  17045  frgpup3lem  17427  gsumval3eu  17538  gsumval3  17541  gsumzaddlem  17554  gsumzmhm  17570  dprdf1o  17665  mplsubglem  18658  evlssca  18745  evls1val  18909  evls1sca  18912  evl1val  18917  gsumfsum  19034  frgpcyg  19144  zrhpsgninv  19153  zrhpsgnevpm  19159  zrhpsgnodpm  19160  mdetralt  19633  mdetunilem7  19643  cpmadumatpoly  19907  chcoeffeqlem  19909  cnpco  20283  lmcnp  20320  upxp  20638  uptx  20640  cnmpt11  20678  cnmpt21  20686  xkofvcn  20699  prdstmdd  21138  prdstgpd  21139  comet  21528  prdsxmslem2  21544  nrmmetd  21589  isngp3  21612  ngpds  21617  tngnm  21659  nmoco  21758  cnmetdval  21791  climcncf  21932  cncfco  21939  htpyco1  22009  htpyco2  22010  phtpyco2  22021  reparphti  22028  copco  22049  pi1cof  22090  pi1coghm  22092  caubl  22277  caublcls  22278  cniccbdd  22412  ovolfioo  22420  ovolficc  22421  ovolfsval  22423  ovolicc2lem1  22470  ovolicc2lem4OLD  22473  ovolicc2lem4  22474  ovolicc2lem5  22475  volsup  22509  uniiccdif  22535  uniioovol  22536  uniiccvol  22537  uniioombllem2  22540  uniioombllem2OLD  22541  uniioombllem3a  22542  uniioombllem4  22544  uniioombllem5  22545  mbfimaopnlem  22611  limccnp  22846  dvcobr  22900  dvcjbr  22903  dvfre  22905  plycjlem  23230  plycj  23231  coecj  23232  radcnvlem2  23369  radcnvlem3  23370  radcnvlt2  23374  pserulm  23377  resinf1o  23485  jensen  23914  eflgam  23970  ftalem3  23999  dchrinv  24189  dchr2sum  24201  dchrisum0re  24351  motco  24585  motcgrg  24589  ex-co  25888  vafval  26222  smfval  26224  vsfval  26254  imsdval  26318  lnocoi  26398  occllem  26956  hocoi  27417  homco1  27454  counop  27574  homco2  27630  hmopco  27676  nlelchi  27714  kbass2  27770  kbass5  27773  leopsq  27782  hmopidmchi  27804  elpjrn  27843  pjinvari  27844  derangenlem  29894  subfacp1lem5  29907  cnpcon  29953  txsconlem  29963  txscon  29964  cvmliftmolem1  30004  cvmliftlem7  30014  cvmlift2lem3  30028  cvmlift2lem7  30032  cvmlift2lem9  30034  cvmliftphtlem  30040  cvmlift3lem1  30042  cvmlift3lem2  30043  cvmlift3lem4  30045  cvmlift3lem5  30046  cvmlift3lem6  30047  cvmlift3lem7  30048  mrsubco  30159  msubco  30169  mclsppslem  30221  sinccvglem  30316  iprodefisumlem  30376  iprodefisum  30377  poimirlem22  31962  mblfinlem2  31978  ftc1anclem5  32021  ftc1anclem8  32024  cocanfo  32044  f1ocan1fv  32053  upixp  32056  ghomco  32181  rngohomco  32213  lautco  33662  ldilco  33681  ltrncoval  33710  tendocoval  34333  tendoconid  34396  tendospass  34587  dicvscacl  34759  cdlemn3  34765  cdlemn9  34773  fvco3d  36604  fvovco  37469  climexp  37683  stoweidlem27  37887  stoweidlem31  37892  mgmhmco  39854
  Copyright terms: Public domain W3C validator