Theorem fvco3 6960

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ∘ ccom 5642   Fn wfn 6506  ⟶wf 6507  ‘cfv 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519

This theorem is referenced by:  fvco3d  6961  foco2  7081  f1cofveqaeqALT  7233  f1ocnvfv1  7251  f1ocnvfv2  7252  fcof1  7262  fcofo  7263  cocan1  7266  cocan2  7267  fveqf1o  7277  isotr  7311  fipreima  9309  fsuppco2  9354  fsuppcor  9355  unxpwdom2  9541  wemapwe  9650  ackbij2lem2  10192  cofsmo  10222  cfcoflem  10225  isf32lem6  10311  isf32lem7  10312  isf32lem8  10313  isf34lem7  10332  isf34lem6  10333  axcc3  10391  axdc4lem  10408  inar1  10728  axdc4uzlem  13948  seqf1olem2  14007  seqf1o  14008  lswco  14805  lo1o1  15498  o1co  15552  caucvgrlem2  15641  summolem3  15680  fsumf1o  15689  fsumcl2lem  15697  fsumadd  15706  fsummulc2  15750  fsumrelem  15773  supcvg  15822  prodmolem3  15899  fprodf1o  15912  fprodser  15915  fprodcl2lem  15916  fprodmul  15926  fproddiv  15927  fprodn0  15945  ruclem11  16208  ruclem12  16209  algcvg  16546  eulerthlem2  16752  cofu1  17846  cofu2  17848  cofucl  17850  fucidcl  17930  fuclid  17931  fucrid  17932  homadm  18002  homacd  18003  evlfcl  18183  curfuncf  18199  yonedalem4c  18238  yonedalem3b  18240  mgmhmco  18641  mhmco  18750  prdspjmhm  18756  pwsco1mhm  18759  lactghmga  19335  frgpup3lem  19707  gsumval3eu  19834  gsumval3  19837  gsumzaddlem  19851  gsumzmhm  19867  dprdf1o  19964  gsumfsum  21351  zrhpsgninv  21494  zrhpsgnevpm  21500  zrhpsgnodpm  21501  evlssca  21996  evls1val  22207  evls1sca  22210  evl1val  22216  mdetralt  22495  mdetunilem7  22505  cpmadumatpoly  22770  chcoeffeqlem  22772  cnpco  23154  lmcnp  23191  upxp  23510  uptx  23512  cnmpt11  23550  cnmpt21  23558  xkofvcn  23571  prdstmdd  24011  prdstgpd  24012  comet  24401  prdsxmslem2  24417  nrmmetd  24462  isngp3  24486  ngpds  24492  tngnm  24539  nmoco  24625  cnmetdval  24658  climcncf  24793  cncfco  24800  htpyco1  24877  htpyco2  24878  phtpyco2  24889  reparphti  24896  reparphtiOLD  24897  copco  24918  pi1cof  24959  pi1coghm  24961  caubl  25208  caublcls  25209  cniccbdd  25362  ovolfioo  25368  ovolficc  25369  ovolfsval  25371  ovolicc2lem1  25418  ovolicc2lem4  25421  ovolicc2lem5  25422  volsup  25457  uniiccdif  25479  uniioovol  25480  uniiccvol  25481  uniioombllem2  25484  uniioombllem3a  25485  uniioombllem4  25487  uniioombllem5  25488  mbfimaopnlem  25556  limccnp  25792  dvcobr  25849  dvcobrOLD  25850  dvcjbr  25853  dvfre  25855  plycjlem  26182  plycj  26183  coecj  26184  plycjOLD  26185  coecjOLD  26186  radcnvlem2  26323  radcnvlem3  26324  radcnvlt2  26328  pserulm  26331  resinf1o  26445  jensen  26899  eflgam  26955  ftalem3  26985  dchrinv  27172  dchr2sum  27184  dchrisum0re  27424  motco  28467  motcgrg  28471  ex-co  30367  vafval  30532  smfval  30534  vsfval  30562  imsdval  30615  lnocoi  30686  occllem  31232  hocoi  31693  homco1  31730  counop  31850  homco2  31906  hmopco  31952  nlelchi  31990  kbass2  32046  kbass5  32049  leopsq  32058  hmopidmchi  32080  elpjrn  32119  pjinvari  32120  cycpmco2  33090  derangenlem  35158  subfacp1lem5  35171  cnpconn  35217  txsconnlem  35227  txsconn  35228  cvmliftmolem1  35268  cvmliftlem7  35278  cvmlift2lem3  35292  cvmlift2lem7  35296  cvmlift2lem9  35298  cvmliftphtlem  35304  cvmlift3lem1  35306  cvmlift3lem2  35307  cvmlift3lem4  35309  cvmlift3lem5  35310  cvmlift3lem6  35311  cvmlift3lem7  35312  mrsubco  35508  msubco  35518  mclsppslem  35570  sinccvglem  35659  iprodefisumlem  35727  iprodefisum  35728  poimirlem22  37636  mblfinlem2  37652  ftc1anclem5  37691  ftc1anclem8  37694  cocanfo  37713  f1ocan1fv  37720  upixp  37723  ghomco  37885  rngohomco  37968  lautco  40091  ldilco  40110  ltrncoval  40139  tendocoval  40760  tendoconid  40823  tendospass  41013  dicvscacl  41185  cdlemn3  41191  cdlemn9  41199  brcoffn  44019  fvovco  45187  climexp  45603  stoweidlem27  46025  stoweidlem31  46029  ovolval4lem1  46647  gricushgr  47917  uspgrlimlem3  47989  uspgrlimlem4  47990  grlictr  48007