Theorem fvco3 6979

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

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

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 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541

This theorem is used by:  fvco3d  6980  foco2  7103  f1cofveqaeqALT  7256  f1ocnvfv1  7278  f1ocnvfv2  7279  fcof1  7289  fcofo  7290  cocan1  7293  cocan2  7294  fveqf1o  7304  isotr  7338  fipreima  9326  fsuppco2  9374  fsuppcor  9375  unxpwdom2  9561  wemapwe  9677  ackbij2lem2  10242  cofsmo  10272  cfcoflem  10275  isf32lem6  10361  isf32lem7  10362  isf32lem8  10363  isf34lem7  10382  isf34lem6  10383  axcc3  10441  axdc4lem  10458  inar1  10785  axdc4uzlem  14048  seqf1olem2  14107  seqf1o  14108  lswco  14911  lo1o1  15620  o1co  15674  caucvgrlem2  15763  summolem3  15801  fsumf1o  15810  fsumcl2lem  15818  fsumadd  15827  fsummulc2  15871  fsumrelem  15895  supcvg  15946  prodmolem3  16021  fprodf1o  16034  fprodser  16037  fprodcl2lem  16038  fprodmul  16048  fproddiv  16049  fprodn0  16067  ruclem11  16329  ruclem12  16330  algcvg  16667  eulerthlem2  16874  cofu1  17974  cofu2  17976  cofucl  17978  fucidcl  18058  fuclid  18059  fucrid  18060  homadm  18130  homacd  18131  evlfcl  18311  curfuncf  18327  yonedalem4c  18366  yonedalem3b  18368  mgmhmco  18817  mhmco  18933  prdspjmhm  18939  pwsco1mhm  18942  lactghmga  19533  frgpup3lem  19905  gsumval3eu  20032  gsumval3  20035  gsumzaddlem  20049  gsumzmhm  20065  dprdf1o  20162  gsumfsum  21648  zrhpsgninv  21799  zrhpsgnevpm  21805  zrhpsgnodpm  21806  evlssca  22311  evls1val  22546  evls1sca  22549  evl1val  22555  mdetralt  22831  mdetunilem7  22841  cpmadumatpoly  23109  chcoeffeqlem  23111  cnpco  23493  lmcnp  23530  upxp  23850  uptx  23852  cnmpt11  23890  cnmpt21  23898  xkofvcn  23911  prdstmdd  24351  prdstgpd  24352  comet  24740  prdsxmslem2  24756  nrmmetd  24801  isngp3  24825  ngpds  24831  tngnm  24878  nmoco  24964  cnmetdval  24997  climcncf  25129  cncfco  25136  htpyco1  25207  htpyco2  25208  phtpyco2  25219  reparphti  25226  copco  25247  pi1cof  25288  pi1coghm  25290  caubl  25537  caublcls  25538  cniccbdd  25690  ovolfioo  25696  ovolficc  25697  ovolfsval  25699  ovolicc2lem1  25746  ovolicc2lem4  25749  ovolicc2lem5  25750  volsup  25785  uniiccdif  25807  uniioovol  25808  uniiccvol  25809  uniioombllem2  25812  uniioombllem3a  25813  uniioombllem4  25815  uniioombllem5  25816  mbfimaopnlem  25884  limccnp  26119  dvcobr  26174  dvcjbr  26177  dvfre  26179  plycjlem  26503  plycj  26504  coecj  26505  plycjOLD  26506  coecjOLD  26507  radcnvlem2  26651  radcnvlem3  26652  radcnvlt2  26656  pserulm  26659  resinf1o  26774  jensen  27226  eflgam  27282  ftalem3  27312  dchrinv  27498  dchr2sum  27510  dchrisum0re  27750  motco  28883  motcgrg  28887  ex-co  30919  vafval  31085  smfval  31087  vsfval  31115  imsdval  31168  lnocoi  31239  occllem  31785  hocoi  32246  homco1  32283  counop  32403  homco2  32459  hmopco  32505  nlelchi  32543  kbass2  32599  kbass5  32602  leopsq  32611  hmopidmchi  32633  elpjrn  32672  pjinvari  32673  cycpmco2  33574  derangenlem  35751  subfacp1lem5  35764  cnpconn  35810  txsconnlem  35820  txsconn  35821  cvmliftmolem1  35861  cvmliftlem7  35871  cvmlift2lem3  35885  cvmlift2lem7  35889  cvmlift2lem9  35891  cvmliftphtlem  35897  cvmlift3lem1  35899  cvmlift3lem2  35900  cvmlift3lem4  35902  cvmlift3lem5  35903  cvmlift3lem6  35904  cvmlift3lem7  35905  mrsubco  36101  msubco  36111  mclsppslem  36163  sinccvglem  36252  iprodefisumlem  36320  iprodefisum  36321  poimirlem22  38392  mblfinlem2  38408  ftc1anclem5  38447  ftc1anclem8  38450  cocanfo  38470  f1ocan1fv  38477  upixp  38480  ghomco  38642  rngohomco  38725  lautco  40971  ldilco  40990  ltrncoval  41019  tendocoval  41640  tendoconid  41703  tendospass  41893  dicvscacl  42065  cdlemn3  42071  cdlemn9  42079  brcoffn  44871  fvovco  46026  climexp  46436  stoweidlem27  46856  stoweidlem31  46860  ovolval4lem1  47478  sqrtnpoly  47762  gricushgr  48834  uspgrlimlem3  48907  uspgrlimlem4  48908  grlictr  48932