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 2146   ∘ ccom 5667   Fn wfn 6535  ⟶wf 6536  ‘cfv 6540

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548

This theorem is used by:  fvco3d  6986  foco2  7108  f1cofveqaeqALT  7261  f1ocnvfv1  7283  f1ocnvfv2  7284  fcof1  7294  fcofo  7295  cocan1  7298  cocan2  7299  fveqf1o  7309  isotr  7343  fipreima  9322  fsuppco2  9370  fsuppcor  9371  unxpwdom2  9557  wemapwe  9673  ackbij2lem2  10238  cofsmo  10268  cfcoflem  10271  isf32lem6  10357  isf32lem7  10358  isf32lem8  10359  isf34lem7  10378  isf34lem6  10379  axcc3  10437  axdc4lem  10454  inar1  10775  axdc4uzlem  14037  seqf1olem2  14096  seqf1o  14097  lswco  14900  lo1o1  15607  o1co  15661  caucvgrlem2  15750  summolem3  15788  fsumf1o  15797  fsumcl2lem  15805  fsumadd  15814  fsummulc2  15858  fsumrelem  15882  supcvg  15933  prodmolem3  16010  fprodf1o  16023  fprodser  16026  fprodcl2lem  16027  fprodmul  16037  fproddiv  16038  fprodn0  16056  ruclem11  16318  ruclem12  16319  algcvg  16656  eulerthlem2  16863  cofu1  17963  cofu2  17965  cofucl  17967  fucidcl  18047  fuclid  18048  fucrid  18049  homadm  18119  homacd  18120  evlfcl  18300  curfuncf  18316  yonedalem4c  18355  yonedalem3b  18357  mgmhmco  18804  mhmco  18919  prdspjmhm  18925  pwsco1mhm  18928  lactghmga  19519  frgpup3lem  19891  gsumval3eu  20018  gsumval3  20021  gsumzaddlem  20035  gsumzmhm  20051  dprdf1o  20148  gsumfsum  21634  zrhpsgninv  21785  zrhpsgnevpm  21791  zrhpsgnodpm  21792  evlssca  22295  evls1val  22530  evls1sca  22533  evl1val  22539  mdetralt  22815  mdetunilem7  22825  cpmadumatpoly  23090  chcoeffeqlem  23092  cnpco  23474  lmcnp  23511  upxp  23831  uptx  23833  cnmpt11  23871  cnmpt21  23879  xkofvcn  23892  prdstmdd  24332  prdstgpd  24333  comet  24721  prdsxmslem2  24737  nrmmetd  24782  isngp3  24806  ngpds  24812  tngnm  24859  nmoco  24945  cnmetdval  24978  climcncf  25110  cncfco  25117  htpyco1  25188  htpyco2  25189  phtpyco2  25200  reparphti  25207  copco  25228  pi1cof  25269  pi1coghm  25271  caubl  25518  caublcls  25519  cniccbdd  25671  ovolfioo  25677  ovolficc  25678  ovolfsval  25680  ovolicc2lem1  25727  ovolicc2lem4  25730  ovolicc2lem5  25731  volsup  25766  uniiccdif  25788  uniioovol  25789  uniiccvol  25790  uniioombllem2  25793  uniioombllem3a  25794  uniioombllem4  25796  uniioombllem5  25797  mbfimaopnlem  25865  limccnp  26101  dvcobr  26156  dvcjbr  26159  dvfre  26161  plycjlem  26484  plycj  26485  coecj  26486  plycjOLD  26487  coecjOLD  26488  radcnvlem2  26628  radcnvlem3  26629  radcnvlt2  26633  pserulm  26636  resinf1o  26752  jensen  27204  eflgam  27260  ftalem3  27290  dchrinv  27476  dchr2sum  27488  dchrisum0re  27728  motco  28860  motcgrg  28864  ex-co  30860  vafval  31026  smfval  31028  vsfval  31056  imsdval  31109  lnocoi  31180  occllem  31726  hocoi  32187  homco1  32224  counop  32344  homco2  32400  hmopco  32446  nlelchi  32484  kbass2  32540  kbass5  32543  leopsq  32552  hmopidmchi  32574  elpjrn  32613  pjinvari  32614  cycpmco2  33517  derangenlem  35700  subfacp1lem5  35713  cnpconn  35759  txsconnlem  35769  txsconn  35770  cvmliftmolem1  35810  cvmliftlem7  35820  cvmlift2lem3  35834  cvmlift2lem7  35838  cvmlift2lem9  35840  cvmliftphtlem  35846  cvmlift3lem1  35848  cvmlift3lem2  35849  cvmlift3lem4  35851  cvmlift3lem5  35852  cvmlift3lem6  35853  cvmlift3lem7  35854  mrsubco  36050  msubco  36060  mclsppslem  36112  sinccvglem  36201  iprodefisumlem  36269  iprodefisum  36270  poimirlem22  38350  mblfinlem2  38366  ftc1anclem5  38405  ftc1anclem8  38408  cocanfo  38428  f1ocan1fv  38435  upixp  38438  ghomco  38600  rngohomco  38683  lautco  40929  ldilco  40948  ltrncoval  40977  tendocoval  41598  tendoconid  41661  tendospass  41851  dicvscacl  42023  cdlemn3  42029  cdlemn9  42037  brcoffn  44814  fvovco  45969  climexp  46379  stoweidlem27  46799  stoweidlem31  46803  ovolval4lem1  47421  gricushgr  48740  uspgrlimlem3  48813  uspgrlimlem4  48814  grlictr  48838