Theorem fvco3 6991

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1534   ∈ wcel 2099   ∘ ccom 5676   Fn wfn 6537  ⟶wf 6538  ‘cfv 6542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5293  ax-nul 5300  ax-pr 5423

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2937  df-ral 3058  df-rex 3067  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fv 6550

This theorem is referenced by:  fvco3d  6992  foco2  7113  f1cofveqaeqALT  7263  f1ocnvfv1  7279  f1ocnvfv2  7280  fcof1  7290  fcofo  7291  cocan1  7294  cocan2  7295  fveqf1o  7306  isotr  7338  fipreima  9376  fsuppco2  9420  fsuppcor  9421  unxpwdom2  9605  wemapwe  9714  ackbij2lem2  10257  cofsmo  10286  cfcoflem  10289  isf32lem6  10375  isf32lem7  10376  isf32lem8  10377  isf34lem7  10396  isf34lem6  10397  axcc3  10455  axdc4lem  10472  inar1  10792  axdc4uzlem  13974  seqf1olem2  14033  seqf1o  14034  lswco  14816  lo1o1  15502  o1co  15556  caucvgrlem2  15647  summolem3  15686  fsumf1o  15695  fsumcl2lem  15703  fsumadd  15712  fsummulc2  15756  fsumrelem  15779  supcvg  15828  prodmolem3  15903  fprodf1o  15916  fprodser  15919  fprodcl2lem  15920  fprodmul  15930  fproddiv  15931  fprodn0  15949  ruclem11  16210  ruclem12  16211  algcvg  16540  eulerthlem2  16744  cofu1  17863  cofu2  17865  cofucl  17867  fucidcl  17950  fuclid  17951  fucrid  17952  homadm  18022  homacd  18023  evlfcl  18207  curfuncf  18223  yonedalem4c  18262  yonedalem3b  18264  mgmhmco  18667  mhmco  18768  prdspjmhm  18774  pwsco1mhm  18777  lactghmga  19353  frgpup3lem  19725  gsumval3eu  19852  gsumval3  19855  gsumzaddlem  19869  gsumzmhm  19885  dprdf1o  19982  gsumfsum  21360  zrhpsgninv  21510  zrhpsgnevpm  21516  zrhpsgnodpm  21517  evlssca  22028  evls1val  22232  evls1sca  22235  evl1val  22241  mdetralt  22503  mdetunilem7  22513  cpmadumatpoly  22778  chcoeffeqlem  22780  cnpco  23164  lmcnp  23201  upxp  23520  uptx  23522  cnmpt11  23560  cnmpt21  23568  xkofvcn  23581  prdstmdd  24021  prdstgpd  24022  comet  24415  prdsxmslem2  24431  nrmmetd  24476  isngp3  24500  ngpds  24506  tngnm  24561  nmoco  24647  cnmetdval  24680  climcncf  24813  cncfco  24820  htpyco1  24897  htpyco2  24898  phtpyco2  24909  reparphti  24916  reparphtiOLD  24917  copco  24938  pi1cof  24979  pi1coghm  24981  caubl  25229  caublcls  25230  cniccbdd  25383  ovolfioo  25389  ovolficc  25390  ovolfsval  25392  ovolicc2lem1  25439  ovolicc2lem4  25442  ovolicc2lem5  25443  volsup  25478  uniiccdif  25500  uniioovol  25501  uniiccvol  25502  uniioombllem2  25505  uniioombllem3a  25506  uniioombllem4  25508  uniioombllem5  25509  mbfimaopnlem  25577  limccnp  25813  dvcobr  25870  dvcobrOLD  25871  dvcjbr  25874  dvfre  25876  plycjlem  26204  plycj  26205  coecj  26206  radcnvlem2  26343  radcnvlem3  26344  radcnvlt2  26348  pserulm  26351  resinf1o  26463  jensen  26914  eflgam  26970  ftalem3  27000  dchrinv  27187  dchr2sum  27199  dchrisum0re  27439  motco  28337  motcgrg  28341  ex-co  30241  vafval  30406  smfval  30408  vsfval  30436  imsdval  30489  lnocoi  30560  occllem  31106  hocoi  31567  homco1  31604  counop  31724  homco2  31780  hmopco  31826  nlelchi  31864  kbass2  31920  kbass5  31923  leopsq  31932  hmopidmchi  31954  elpjrn  31993  pjinvari  31994  cycpmco2  32848  derangenlem  34775  subfacp1lem5  34788  cnpconn  34834  txsconnlem  34844  txsconn  34845  cvmliftmolem1  34885  cvmliftlem7  34895  cvmlift2lem3  34909  cvmlift2lem7  34913  cvmlift2lem9  34915  cvmliftphtlem  34921  cvmlift3lem1  34923  cvmlift3lem2  34924  cvmlift3lem4  34926  cvmlift3lem5  34927  cvmlift3lem6  34928  cvmlift3lem7  34929  mrsubco  35125  msubco  35135  mclsppslem  35187  sinccvglem  35270  iprodefisumlem  35328  iprodefisum  35329  poimirlem22  37109  mblfinlem2  37125  ftc1anclem5  37164  ftc1anclem8  37167  cocanfo  37186  f1ocan1fv  37193  upixp  37196  ghomco  37358  rngohomco  37441  lautco  39564  ldilco  39583  ltrncoval  39612  tendocoval  40233  tendoconid  40296  tendospass  40486  dicvscacl  40658  cdlemn3  40664  cdlemn9  40672  brcoffn  43454  fvovco  44560  climexp  44987  stoweidlem27  45409  stoweidlem31  45413  ovolval4lem1  46031  gricushgr  47177

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »