Theorem fvco3 6632

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

Step	Hyp	Ref	Expression
1		ffn 6387	. 2 ⊢ (𝐺:𝐴⟶𝐵 → 𝐺 Fn 𝐴)
2		fvco2 6630	. 2 ⊢ ((𝐺 Fn 𝐴 ∧ 𝐶 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶)))
3	1, 2	sylan 580	1 ⊢ ((𝐺:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶)))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1522   ∈ wcel 2081   ∘ ccom 5452   Fn wfn 6225  ⟶wf 6226  ‘cfv 6230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5099  ax-nul 5106  ax-pow 5162  ax-pr 5226

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3710  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-nul 4216  df-if 4386  df-sn 4477  df-pr 4479  df-op 4483  df-uni 4750  df-br 4967  df-opab 5029  df-id 5353  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-rn 5459  df-res 5460  df-ima 5461  df-iota 6194  df-fun 6232  df-fn 6233  df-f 6234  df-fv 6238

This theorem is referenced by:  fvco3d  6633  foco2  6741  f1cofveqaeqALT  6887  f1ocnvfv1  6903  f1ocnvfv2  6904  fcof1  6913  fcofo  6914  cocan1  6917  cocan2  6918  fveqf1o  6928  isotr  6957  algrflem  7677  fipreima  8681  fsuppco2  8717  fsuppcor  8718  unxpwdom2  8903  wemapwe  9011  ackbij2lem2  9513  cofsmo  9542  cfcoflem  9545  isf32lem6  9631  isf32lem7  9632  isf32lem8  9633  isf34lem7  9652  isf34lem6  9653  axcc3  9711  axdc4lem  9728  canthp1lem2  9926  inar1  10048  axdc4uzlem  13206  seqf1olem2  13265  seqf1o  13266  lswco  14042  lo1o1  14728  o1co  14782  caucvgrlem2  14870  summolem3  14909  fsumf1o  14918  fsumcl2lem  14926  fsumadd  14934  fsummulc2  14977  fsumrelem  15000  supcvg  15049  prodmolem3  15125  fprodf1o  15138  fprodser  15141  fprodcl2lem  15142  fprodmul  15152  fproddiv  15153  fprodn0  15171  ruclem11  15431  ruclem12  15432  algcvg  15754  eulerthlem2  15953  cofu1  16988  cofu2  16990  cofucl  16992  fucidcl  17069  fuclid  17070  fucrid  17071  homadm  17134  homacd  17135  evlfcl  17306  curfuncf  17322  yonedalem4c  17361  yonedalem3b  17363  yonedainv  17365  mhmco  17806  prdspjmhm  17811  pwsco1mhm  17814  lactghmga  18268  frgpup3lem  18635  gsumval3eu  18750  gsumval3  18753  gsumzaddlem  18766  gsumzmhm  18782  dprdf1o  18876  mplsubglem  19907  evlssca  19994  evls1val  20171  evls1sca  20174  evl1val  20179  gsumfsum  20299  frgpcyg  20407  zrhpsgninv  20416  zrhpsgnevpm  20422  zrhpsgnodpm  20423  mdetralt  20906  mdetunilem7  20916  cpmadumatpoly  21180  chcoeffeqlem  21182  cnpco  21564  lmcnp  21601  upxp  21920  uptx  21922  cnmpt11  21960  cnmpt21  21968  xkofvcn  21981  prdstmdd  22420  prdstgpd  22421  comet  22811  prdsxmslem2  22827  nrmmetd  22872  isngp3  22895  ngpds  22901  tngnm  22948  nmoco  23034  cnmetdval  23067  climcncf  23196  cncfco  23203  htpyco1  23270  htpyco2  23271  phtpyco2  23282  reparphti  23289  copco  23310  pi1cof  23351  pi1coghm  23353  caubl  23599  caublcls  23600  cniccbdd  23750  ovolfioo  23756  ovolficc  23757  ovolfsval  23759  ovolicc2lem1  23806  ovolicc2lem4  23809  ovolicc2lem5  23810  volsup  23845  uniiccdif  23867  uniioovol  23868  uniiccvol  23869  uniioombllem2  23872  uniioombllem3a  23873  uniioombllem4  23875  uniioombllem5  23876  mbfimaopnlem  23944  limccnp  24177  dvcobr  24231  dvcjbr  24234  dvfre  24236  plycjlem  24554  plycj  24555  coecj  24556  radcnvlem2  24690  radcnvlem3  24691  radcnvlt2  24695  pserulm  24698  resinf1o  24806  jensen  25253  eflgam  25309  ftalem3  25339  dchrinv  25524  dchr2sum  25536  dchrisum0re  25776  motco  26013  motcgrg  26017  ex-co  27914  vafval  28076  smfval  28078  vsfval  28106  imsdval  28159  lnocoi  28230  occllem  28776  hocoi  29237  homco1  29274  counop  29394  homco2  29450  hmopco  29496  nlelchi  29534  kbass2  29590  kbass5  29593  leopsq  29602  hmopidmchi  29624  elpjrn  29663  pjinvari  29664  derangenlem  32032  subfacp1lem5  32045  cnpconn  32091  txsconnlem  32101  txsconn  32102  cvmliftmolem1  32142  cvmliftlem7  32152  cvmlift2lem3  32166  cvmlift2lem7  32170  cvmlift2lem9  32172  cvmliftphtlem  32178  cvmlift3lem1  32180  cvmlift3lem2  32181  cvmlift3lem4  32183  cvmlift3lem5  32184  cvmlift3lem6  32185  cvmlift3lem7  32186  mrsubco  32382  msubco  32392  mclsppslem  32444  sinccvglem  32529  iprodefisumlem  32586  iprodefisum  32587  poimirlem22  34470  mblfinlem2  34486  ftc1anclem5  34527  ftc1anclem8  34530  cocanfo  34550  f1ocan1fv  34558  upixp  34561  ghomco  34726  rngohomco  34809  lautco  36789  ldilco  36808  ltrncoval  36837  tendocoval  37458  tendoconid  37521  tendospass  37711  dicvscacl  37883  cdlemn3  37889  cdlemn9  37897  brcoffn  39890  fvovco  41020  climexp  41453  stoweidlem27  41880  stoweidlem31  41884  ovolval4lem1  42499  isomushgr  43499  mgmhmco  43576