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

Theorem fvco3 5935
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 5722 . 2  |-  ( G : A --> B  ->  G  Fn  A )
2 fvco2 5933 . 2  |-  ( ( G  Fn  A  /\  C  e.  A )  ->  ( ( F  o.  G ) `  C
)  =  ( F `
 ( G `  C ) ) )
31, 2sylan 471 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 369    = wceq 1374    e. wcel 1762    o. ccom 4996    Fn wfn 5574   -->wf 5575   ` cfv 5579
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-fv 5587
This theorem is referenced by:  foco2  6032  f1ocnvfv1  6161  f1ocnvfv2  6162  fcof1  6169  fcofo  6170  cocan1  6173  cocan2  6174  fveqf1o  6184  isotr  6211  algrflem  6882  fipreima  7815  fsuppco2  7851  fsuppcor  7852  unxpwdom2  8003  wemapwe  8128  wemapweOLD  8129  ackbij2lem2  8609  cofsmo  8638  cfcoflem  8641  isf32lem6  8727  isf32lem7  8728  isf32lem8  8729  isf34lem7  8748  isf34lem6  8749  axcc3  8807  axdc4lem  8824  canthp1lem2  9020  inar1  9142  axdc4uzlem  12048  seqf1olem2  12103  seqf1o  12104  lswco  12754  lo1o1  13304  o1co  13358  caucvgrlem2  13446  summolem3  13485  fsumf1o  13494  fsumcl2lem  13502  fsumadd  13510  fsummulc2  13548  fsumrelem  13570  supcvg  13619  ruclem11  13823  ruclem12  13824  algcvg  14053  eulerthlem2  14160  cofu1  15100  cofu2  15102  cofucl  15104  fucidcl  15181  fuclid  15182  fucrid  15183  homadm  15214  homacd  15215  evlfcl  15338  curfuncf  15354  yonedalem4c  15393  yonedalem3b  15395  yonedainv  15397  mhmco  15796  prdspjmhm  15801  pwsco1mhm  15804  lactghmga  16217  frgpup3lem  16584  gsumval3eu  16691  gsumval3OLD  16692  gsumval3  16695  gsumzaddlem  16718  gsumzaddlemOLD  16720  gsumzmhm  16741  gsumzmhmOLD  16742  gsumzinvOLD  16754  gsumsubOLD  16759  dprdf1o  16862  mplsubglem  17857  mplsubglemOLD  17859  evlssca  17955  evls1val  18121  evls1sca  18124  evl1val  18129  gsumfsum  18245  frgpcyg  18372  zrhpsgninv  18381  zrhpsgnevpm  18387  zrhpsgnodpm  18388  mdetralt  18870  mdetunilem7  18880  cpmadumatpoly  19144  chcoeffeqlem  19146  cnpco  19527  lmcnp  19564  upxp  19852  uptx  19854  cnmpt11  19892  cnmpt21  19900  xkofvcn  19913  prdstmdd  20350  prdstgpd  20351  comet  20744  prdsxmslem2  20760  nrmmetd  20823  isngp3  20846  ngpds  20851  tngnm  20893  nmoco  20972  cnmetdval  21006  climcncf  21132  cncfco  21139  htpyco1  21206  htpyco2  21207  phtpyco2  21218  reparphti  21225  copco  21246  pi1cof  21287  pi1coghm  21289  caubl  21474  caublcls  21475  cniccbdd  21601  ovolfioo  21607  ovolficc  21608  ovolfsval  21610  ovolicc2lem1  21656  ovolicc2lem4  21659  ovolicc2lem5  21660  volsup  21694  uniiccdif  21715  uniioovol  21716  uniiccvol  21717  uniioombllem2  21720  uniioombllem3a  21721  uniioombllem4  21723  uniioombllem5  21724  mbfimaopnlem  21790  limccnp  22023  dvcobr  22077  dvcjbr  22080  dvfre  22082  plycjlem  22400  plycj  22401  coecj  22402  radcnvlem2  22536  radcnvlem3  22537  radcnvlt2  22541  pserulm  22544  resinf1o  22649  jensen  23039  ftalem3  23069  dchrinv  23257  dchr2sum  23269  dchrisum0re  23419  motco  23648  motcgrg  23652  ex-co  24686  vafval  25022  smfval  25024  vsfval  25054  imsdval  25118  lnocoi  25198  occllem  25747  hocoi  26209  homco1  26246  counop  26366  homco2  26422  hmopco  26468  nlelchi  26506  kbass2  26562  kbass5  26565  leopsq  26574  hmopidmchi  26596  elpjrn  26635  pjinvari  26636  eflgam  28077  derangenlem  28105  subfacp1lem5  28118  cnpcon  28165  txsconlem  28175  txscon  28176  cvmliftmolem1  28216  cvmliftlem7  28226  cvmlift2lem3  28240  cvmlift2lem7  28244  cvmlift2lem9  28246  cvmliftphtlem  28252  cvmlift3lem1  28254  cvmlift3lem2  28255  cvmlift3lem4  28257  cvmlift3lem5  28258  cvmlift3lem6  28259  cvmlift3lem7  28260  sinccvglem  28363  prodmolem3  28492  fprodf1o  28505  fprodser  28508  fprodcl2lem  28509  fprodmul  28517  fproddiv  28518  fprodn0  28536  iprodefisumlem  28550  iprodefisum  28551  mblfinlem2  29480  ftc1anclem5  29522  ftc1anclem8  29525  cocanfo  29662  f1ocan1fv  29671  upixp  29674  ghomco  29799  rngohomco  29831  climexp  30966  stoweidlem27  31146  stoweidlem31  31150  lautco  34768  ldilco  34787  ltrncoval  34816  tendocoval  35437  tendoconid  35500  tendospass  35691  dicvscacl  35863  cdlemn3  35869  cdlemn9  35877
  Copyright terms: Public domain W3C validator