Theorem fvco3 7016

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147   ∘ ccom 5662   Fn wfn 6561  ⟶wf 6562  ‘cfv 6566

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-fv 6574

This theorem is used by:  fvco3d  7017  foco2  7141  f1cofveqaeqALT  7293  f1ocnvfv1  7315  f1ocnvfv2  7316  fcof1  7326  fcofo  7327  cocan1  7330  cocan2  7331  fveqf1o  7341  isotr  7375  fipreima  9385  fsuppco2  9432  fsuppcor  9433  unxpwdom2  9619  wemapwe  9735  ackbij2lem2  10356  cofsmo  10386  cfcoflem  10389  isf32lem6  10475  isf32lem7  10476  isf32lem8  10477  isf34lem7  10496  isf34lem6  10497  axcc3  10555  axdc4lem  10572  inar1  10899  axdc4uzlem  14166  seqf1olem2  14225  seqf1o  14226  lswco  15032  lo1o1  15743  o1co  15797  caucvgrlem2  15886  summolem3  15924  fsumf1o  15933  fsumcl2lem  15941  fsumadd  15950  fsummulc2  15994  fsumrelem  16018  supcvg  16069  prodmolem3  16144  fprodf1o  16157  fprodser  16160  fprodcl2lem  16161  fprodmul  16171  fproddiv  16172  fprodn0  16190  ruclem11  16452  ruclem12  16453  algcvg  16795  eulerthlem2  17003  cofu1  18109  cofu2  18111  cofucl  18113  fucidcl  18193  fuclid  18194  fucrid  18195  homadm  18265  homacd  18266  evlfcl  18446  curfuncf  18462  yonedalem4c  18501  yonedalem3b  18503  mgmhmco  18953  mhmco  19069  prdspjmhm  19075  pwsco1mhm  19078  lactghmga  19670  frgpup3lem  20042  gsumval3eu  20169  gsumval3  20172  gsumzaddlem  20186  gsumzmhm  20202  dprdf1o  20299  gsumfsum  21794  zrhpsgninv  21946  zrhpsgnevpm  21952  zrhpsgnodpm  21953  evlssca  22458  evls1val  22693  evls1sca  22696  evl1val  22702  mdetralt  22978  mdetunilem7  22988  cpmadumatpoly  23256  chcoeffeqlem  23258  cnpco  23640  lmcnp  23677  upxp  23997  uptx  23999  cnmpt11  24037  cnmpt21  24045  xkofvcn  24058  prdstmdd  24498  prdstgpd  24499  comet  24887  prdsxmslem2  24903  nrmmetd  24948  isngp3  24972  ngpds  24978  tngnm  25025  nmoco  25111  cnmetdval  25144  climcncf  25276  cncfco  25283  htpyco1  25354  htpyco2  25355  phtpyco2  25366  reparphti  25373  copco  25394  pi1cof  25435  pi1coghm  25437  caubl  25684  caublcls  25685  cniccbdd  25837  ovolfioo  25843  ovolficc  25844  ovolfsval  25846  ovolicc2lem1  25893  ovolicc2lem4  25896  ovolicc2lem5  25897  volsup  25932  uniiccdif  25954  uniioovol  25955  uniiccvol  25956  uniioombllem2  25959  uniioombllem3a  25960  uniioombllem4  25962  uniioombllem5  25963  mbfimaopnlem  26031  limccnp  26266  dvcobr  26321  dvcjbr  26324  dvfre  26326  plycjlem  26650  plycj  26651  coecj  26652  radcnvlem2  26798  radcnvlem3  26799  radcnvlt2  26803  pserulm  26806  resinf1o  26921  jensen  27373  eflgam  27429  ftalem3  27459  dchrinv  27645  dchr2sum  27657  dchrisum0re  27897  motco  29060  motcgrg  29064  ex-co  31096  vafval  31262  smfval  31264  vsfval  31292  imsdval  31345  lnocoi  31416  occllem  31962  hocoi  32423  homco1  32460  counop  32580  homco2  32636  hmopco  32682  nlelchi  32720  kbass2  32776  kbass5  32779  leopsq  32788  hmopidmchi  32810  elpjrn  32849  pjinvari  32850  cycpmco2  33793  derangenlem  36144  subfacp1lem5  36157  cnpconn  36203  txsconnlem  36213  txsconn  36214  cvmliftmolem1  36254  cvmliftlem7  36264  cvmlift2lem3  36278  cvmlift2lem7  36282  cvmlift2lem9  36284  cvmliftphtlem  36290  cvmlift3lem1  36292  cvmlift3lem2  36293  cvmlift3lem4  36295  cvmlift3lem5  36296  cvmlift3lem6  36297  cvmlift3lem7  36298  mrsubco  36494  msubco  36504  mclsppslem  36556  sinccvglem  36645  iprodefisumlem  36720  iprodefisum  36721  poimirlem22  38828  mblfinlem2  38844  ftc1anclem5  38883  ftc1anclem8  38886  cocanfo  38921  f1ocan1fv  38928  upixp  38931  ghomco  39091  rngohomco  39174  lautco  41420  ldilco  41439  ltrncoval  41468  tendocoval  42089  tendoconid  42152  tendospass  42342  dicvscacl  42514  cdlemn3  42520  cdlemn9  42528  brcoffn  45291  fvovco  46481  climexp  46890  stoweidlem27  47310  stoweidlem31  47314  ovolval4lem1  47932  sqrtnpoly  48216  gricushgr  49288  uspgrlimlem3  49361  uspgrlimlem4  49362  grlictr  49386