Theorem fvco3 6993

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2146   ∘ ccom 5658   Fn wfn 6541  ⟶wf 6542  ‘cfv 6546

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-nul 5262  ax-pr 5394

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-opab 5170  df-id 5549  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-fv 6554

This theorem is used by:  fvco3d  6994  foco2  7117  f1cofveqaeqALT  7269  f1ocnvfv1  7291  f1ocnvfv2  7292  fcof1  7302  fcofo  7303  cocan1  7306  cocan2  7307  fveqf1o  7317  isotr  7351  fipreima  9358  fsuppco2  9405  fsuppcor  9406  unxpwdom2  9592  wemapwe  9708  ackbij2lem2  10327  cofsmo  10357  cfcoflem  10360  isf32lem6  10446  isf32lem7  10447  isf32lem8  10448  isf34lem7  10467  isf34lem6  10468  axcc3  10526  axdc4lem  10543  inar1  10870  axdc4uzlem  14136  seqf1olem2  14195  seqf1o  14196  lswco  15001  lo1o1  15711  o1co  15765  caucvgrlem2  15854  summolem3  15892  fsumf1o  15901  fsumcl2lem  15909  fsumadd  15918  fsummulc2  15962  fsumrelem  15986  supcvg  16037  prodmolem3  16112  fprodf1o  16125  fprodser  16128  fprodcl2lem  16129  fprodmul  16139  fproddiv  16140  fprodn0  16158  ruclem11  16420  ruclem12  16421  algcvg  16763  eulerthlem2  16971  cofu1  18071  cofu2  18073  cofucl  18075  fucidcl  18155  fuclid  18156  fucrid  18157  homadm  18227  homacd  18228  evlfcl  18408  curfuncf  18424  yonedalem4c  18463  yonedalem3b  18465  mgmhmco  18915  mhmco  19031  prdspjmhm  19037  pwsco1mhm  19040  lactghmga  19631  frgpup3lem  20003  gsumval3eu  20130  gsumval3  20133  gsumzaddlem  20147  gsumzmhm  20163  dprdf1o  20260  gsumfsum  21752  zrhpsgninv  21903  zrhpsgnevpm  21909  zrhpsgnodpm  21910  evlssca  22415  evls1val  22650  evls1sca  22653  evl1val  22659  mdetralt  22935  mdetunilem7  22945  cpmadumatpoly  23213  chcoeffeqlem  23215  cnpco  23597  lmcnp  23634  upxp  23954  uptx  23956  cnmpt11  23994  cnmpt21  24002  xkofvcn  24015  prdstmdd  24455  prdstgpd  24456  comet  24844  prdsxmslem2  24860  nrmmetd  24905  isngp3  24929  ngpds  24935  tngnm  24982  nmoco  25068  cnmetdval  25101  climcncf  25233  cncfco  25240  htpyco1  25311  htpyco2  25312  phtpyco2  25323  reparphti  25330  copco  25351  pi1cof  25392  pi1coghm  25394  caubl  25641  caublcls  25642  cniccbdd  25794  ovolfioo  25800  ovolficc  25801  ovolfsval  25803  ovolicc2lem1  25850  ovolicc2lem4  25853  ovolicc2lem5  25854  volsup  25889  uniiccdif  25911  uniioovol  25912  uniiccvol  25913  uniioombllem2  25916  uniioombllem3a  25917  uniioombllem4  25919  uniioombllem5  25920  mbfimaopnlem  25988  limccnp  26223  dvcobr  26278  dvcjbr  26281  dvfre  26283  plycjlem  26607  plycj  26608  coecj  26609  radcnvlem2  26753  radcnvlem3  26754  radcnvlt2  26758  pserulm  26761  resinf1o  26876  jensen  27328  eflgam  27384  ftalem3  27414  dchrinv  27600  dchr2sum  27612  dchrisum0re  27852  motco  29015  motcgrg  29019  ex-co  31051  vafval  31217  smfval  31219  vsfval  31247  imsdval  31300  lnocoi  31371  occllem  31917  hocoi  32378  homco1  32415  counop  32535  homco2  32591  hmopco  32637  nlelchi  32675  kbass2  32731  kbass5  32734  leopsq  32743  hmopidmchi  32765  elpjrn  32804  pjinvari  32805  cycpmco2  33747  derangenlem  36057  subfacp1lem5  36070  cnpconn  36116  txsconnlem  36126  txsconn  36127  cvmliftmolem1  36167  cvmliftlem7  36177  cvmlift2lem3  36191  cvmlift2lem7  36195  cvmlift2lem9  36197  cvmliftphtlem  36203  cvmlift3lem1  36205  cvmlift3lem2  36206  cvmlift3lem4  36208  cvmlift3lem5  36209  cvmlift3lem6  36210  cvmlift3lem7  36211  mrsubco  36407  msubco  36417  mclsppslem  36469  sinccvglem  36558  iprodefisumlem  36632  iprodefisum  36633  poimirlem22  38700  mblfinlem2  38716  ftc1anclem5  38755  ftc1anclem8  38758  cocanfo  38793  f1ocan1fv  38800  upixp  38803  ghomco  38965  rngohomco  39048  lautco  41294  ldilco  41313  ltrncoval  41342  tendocoval  41963  tendoconid  42026  tendospass  42216  dicvscacl  42388  cdlemn3  42394  cdlemn9  42402  brcoffn  45170  fvovco  46347  climexp  46756  stoweidlem27  47176  stoweidlem31  47180  ovolval4lem1  47798  sqrtnpoly  48082  gricushgr  49154  uspgrlimlem3  49227  uspgrlimlem4  49228  grlictr  49252