Theorem fvco3 6985

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 6709	. 2 ⊢ (𝐺:𝐴⟶𝐵 → 𝐺 Fn 𝐴)
2		fvco2 6982	. 2 ⊢ ((𝐺 Fn 𝐴 ∧ 𝐶 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶)))
3	1, 2	sylan 592	1 ⊢ ((𝐺:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ∘ ccom 5655   Fn wfn 6533  ⟶wf 6534  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546

This theorem is used by:  fvco3d  6986  foco2  7109  f1cofveqaeqALT  7262  f1ocnvfv1  7284  f1ocnvfv2  7285  fcof1  7295  fcofo  7296  cocan1  7299  cocan2  7300  fveqf1o  7310  isotr  7344  fipreima  9347  fsuppco2  9395  fsuppcor  9396  unxpwdom2  9582  wemapwe  9698  ackbij2lem2  10317  cofsmo  10347  cfcoflem  10350  isf32lem6  10436  isf32lem7  10437  isf32lem8  10438  isf34lem7  10457  isf34lem6  10458  axcc3  10516  axdc4lem  10533  inar1  10860  axdc4uzlem  14126  seqf1olem2  14185  seqf1o  14186  lswco  14990  lo1o1  15699  o1co  15753  caucvgrlem2  15842  summolem3  15880  fsumf1o  15889  fsumcl2lem  15897  fsumadd  15906  fsummulc2  15950  fsumrelem  15974  supcvg  16025  prodmolem3  16100  fprodf1o  16113  fprodser  16116  fprodcl2lem  16117  fprodmul  16127  fproddiv  16128  fprodn0  16146  ruclem11  16408  ruclem12  16409  algcvg  16751  eulerthlem2  16959  cofu1  18059  cofu2  18061  cofucl  18063  fucidcl  18143  fuclid  18144  fucrid  18145  homadm  18215  homacd  18216  evlfcl  18396  curfuncf  18412  yonedalem4c  18451  yonedalem3b  18453  mgmhmco  18903  mhmco  19019  prdspjmhm  19025  pwsco1mhm  19028  lactghmga  19619  frgpup3lem  19991  gsumval3eu  20118  gsumval3  20121  gsumzaddlem  20135  gsumzmhm  20151  dprdf1o  20248  gsumfsum  21740  zrhpsgninv  21891  zrhpsgnevpm  21897  zrhpsgnodpm  21898  evlssca  22403  evls1val  22638  evls1sca  22641  evl1val  22647  mdetralt  22923  mdetunilem7  22933  cpmadumatpoly  23201  chcoeffeqlem  23203  cnpco  23585  lmcnp  23622  upxp  23942  uptx  23944  cnmpt11  23982  cnmpt21  23990  xkofvcn  24003  prdstmdd  24443  prdstgpd  24444  comet  24832  prdsxmslem2  24848  nrmmetd  24893  isngp3  24917  ngpds  24923  tngnm  24970  nmoco  25056  cnmetdval  25089  climcncf  25221  cncfco  25228  htpyco1  25299  htpyco2  25300  phtpyco2  25311  reparphti  25318  copco  25339  pi1cof  25380  pi1coghm  25382  caubl  25629  caublcls  25630  cniccbdd  25782  ovolfioo  25788  ovolficc  25789  ovolfsval  25791  ovolicc2lem1  25838  ovolicc2lem4  25841  ovolicc2lem5  25842  volsup  25877  uniiccdif  25899  uniioovol  25900  uniiccvol  25901  uniioombllem2  25904  uniioombllem3a  25905  uniioombllem4  25907  uniioombllem5  25908  mbfimaopnlem  25976  limccnp  26211  dvcobr  26266  dvcjbr  26269  dvfre  26271  plycjlem  26595  plycj  26596  coecj  26597  radcnvlem2  26741  radcnvlem3  26742  radcnvlt2  26746  pserulm  26749  resinf1o  26864  jensen  27316  eflgam  27372  ftalem3  27402  dchrinv  27588  dchr2sum  27600  dchrisum0re  27840  motco  29003  motcgrg  29007  ex-co  31039  vafval  31205  smfval  31207  vsfval  31235  imsdval  31288  lnocoi  31359  occllem  31905  hocoi  32366  homco1  32403  counop  32523  homco2  32579  hmopco  32625  nlelchi  32663  kbass2  32719  kbass5  32722  leopsq  32731  hmopidmchi  32753  elpjrn  32792  pjinvari  32793  cycpmco2  33694  derangenlem  35936  subfacp1lem5  35949  cnpconn  35995  txsconnlem  36005  txsconn  36006  cvmliftmolem1  36046  cvmliftlem7  36056  cvmlift2lem3  36070  cvmlift2lem7  36074  cvmlift2lem9  36076  cvmliftphtlem  36082  cvmlift3lem1  36084  cvmlift3lem2  36085  cvmlift3lem4  36087  cvmlift3lem5  36088  cvmlift3lem6  36089  cvmlift3lem7  36090  mrsubco  36286  msubco  36296  mclsppslem  36348  sinccvglem  36437  iprodefisumlem  36505  iprodefisum  36506  poimirlem22  38560  mblfinlem2  38576  ftc1anclem5  38615  ftc1anclem8  38618  cocanfo  38653  f1ocan1fv  38660  upixp  38663  ghomco  38825  rngohomco  38908  lautco  41154  ldilco  41173  ltrncoval  41202  tendocoval  41823  tendoconid  41886  tendospass  42076  dicvscacl  42248  cdlemn3  42254  cdlemn9  42262  brcoffn  45029  fvovco  46207  climexp  46616  stoweidlem27  47036  stoweidlem31  47040  ovolval4lem1  47658  sqrtnpoly  47942  gricushgr  49014  uspgrlimlem3  49087  uspgrlimlem4  49088  grlictr  49112