Theorem fvco3 6982

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

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

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 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545

This theorem is used by:  fvco3d  6983  foco2  7106  f1cofveqaeqALT  7259  f1ocnvfv1  7281  f1ocnvfv2  7282  fcof1  7292  fcofo  7293  cocan1  7296  cocan2  7297  fveqf1o  7307  isotr  7341  fipreima  9329  fsuppco2  9377  fsuppcor  9378  unxpwdom2  9564  wemapwe  9680  ackbij2lem2  10245  cofsmo  10275  cfcoflem  10278  isf32lem6  10364  isf32lem7  10365  isf32lem8  10366  isf34lem7  10385  isf34lem6  10386  axcc3  10444  axdc4lem  10461  inar1  10788  axdc4uzlem  14051  seqf1olem2  14110  seqf1o  14111  lswco  14914  lo1o1  15623  o1co  15677  caucvgrlem2  15766  summolem3  15804  fsumf1o  15813  fsumcl2lem  15821  fsumadd  15830  fsummulc2  15874  fsumrelem  15898  supcvg  15949  prodmolem3  16026  fprodf1o  16039  fprodser  16042  fprodcl2lem  16043  fprodmul  16053  fproddiv  16054  fprodn0  16072  ruclem11  16334  ruclem12  16335  algcvg  16672  eulerthlem2  16879  cofu1  17979  cofu2  17981  cofucl  17983  fucidcl  18063  fuclid  18064  fucrid  18065  homadm  18135  homacd  18136  evlfcl  18316  curfuncf  18332  yonedalem4c  18371  yonedalem3b  18373  mgmhmco  18822  mhmco  18938  prdspjmhm  18944  pwsco1mhm  18947  lactghmga  19538  frgpup3lem  19910  gsumval3eu  20037  gsumval3  20040  gsumzaddlem  20054  gsumzmhm  20070  dprdf1o  20167  gsumfsum  21653  zrhpsgninv  21804  zrhpsgnevpm  21810  zrhpsgnodpm  21811  evlssca  22316  evls1val  22551  evls1sca  22554  evl1val  22560  mdetralt  22836  mdetunilem7  22846  cpmadumatpoly  23114  chcoeffeqlem  23116  cnpco  23498  lmcnp  23535  upxp  23855  uptx  23857  cnmpt11  23895  cnmpt21  23903  xkofvcn  23916  prdstmdd  24356  prdstgpd  24357  comet  24745  prdsxmslem2  24761  nrmmetd  24806  isngp3  24830  ngpds  24836  tngnm  24883  nmoco  24969  cnmetdval  25002  climcncf  25134  cncfco  25141  htpyco1  25212  htpyco2  25213  phtpyco2  25224  reparphti  25231  copco  25252  pi1cof  25293  pi1coghm  25295  caubl  25542  caublcls  25543  cniccbdd  25695  ovolfioo  25701  ovolficc  25702  ovolfsval  25704  ovolicc2lem1  25751  ovolicc2lem4  25754  ovolicc2lem5  25755  volsup  25790  uniiccdif  25812  uniioovol  25813  uniiccvol  25814  uniioombllem2  25817  uniioombllem3a  25818  uniioombllem4  25820  uniioombllem5  25821  mbfimaopnlem  25889  limccnp  26125  dvcobr  26180  dvcjbr  26183  dvfre  26185  plycjlem  26509  plycj  26510  coecj  26511  plycjOLD  26512  coecjOLD  26513  radcnvlem2  26657  radcnvlem3  26658  radcnvlt2  26662  pserulm  26665  resinf1o  26781  jensen  27233  eflgam  27289  ftalem3  27319  dchrinv  27505  dchr2sum  27517  dchrisum0re  27757  motco  28890  motcgrg  28894  ex-co  30926  vafval  31092  smfval  31094  vsfval  31122  imsdval  31175  lnocoi  31246  occllem  31792  hocoi  32253  homco1  32290  counop  32410  homco2  32466  hmopco  32512  nlelchi  32550  kbass2  32606  kbass5  32609  leopsq  32618  hmopidmchi  32640  elpjrn  32679  pjinvari  32680  cycpmco2  33581  derangenlem  35758  subfacp1lem5  35771  cnpconn  35817  txsconnlem  35827  txsconn  35828  cvmliftmolem1  35868  cvmliftlem7  35878  cvmlift2lem3  35892  cvmlift2lem7  35896  cvmlift2lem9  35898  cvmliftphtlem  35904  cvmlift3lem1  35906  cvmlift3lem2  35907  cvmlift3lem4  35909  cvmlift3lem5  35910  cvmlift3lem6  35911  cvmlift3lem7  35912  mrsubco  36108  msubco  36118  mclsppslem  36170  sinccvglem  36259  iprodefisumlem  36327  iprodefisum  36328  poimirlem22  38399  mblfinlem2  38415  ftc1anclem5  38454  ftc1anclem8  38457  cocanfo  38477  f1ocan1fv  38484  upixp  38487  ghomco  38649  rngohomco  38732  lautco  40978  ldilco  40997  ltrncoval  41026  tendocoval  41647  tendoconid  41710  tendospass  41900  dicvscacl  42072  cdlemn3  42078  cdlemn9  42086  brcoffn  44878  fvovco  46033  climexp  46443  stoweidlem27  46863  stoweidlem31  46867  ovolval4lem1  47485  sqrtnpoly  47769  gricushgr  48841  uspgrlimlem3  48914  uspgrlimlem4  48915  grlictr  48939