Theorem fvco 6921

Description: Value of a function composition. Similar to Exercise 5 of [TakeutiZaring] p. 28. (Contributed by NM, 22-Apr-2006.) (Proof shortened by Mario Carneiro, 26-Dec-2014.)

Assertion

Ref	Expression
fvco	⊢ ((Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺) → ((𝐹 ∘ 𝐺)‘𝐴) = (𝐹‘(𝐺‘𝐴)))

Proof of Theorem fvco

Step	Hyp	Ref	Expression
1		funfn 6512	. 2 ⊢ (Fun 𝐺 ↔ 𝐺 Fn dom 𝐺)
2		fvco2 6920	. 2 ⊢ ((𝐺 Fn dom 𝐺 ∧ 𝐴 ∈ dom 𝐺) → ((𝐹 ∘ 𝐺)‘𝐴) = (𝐹‘(𝐺‘𝐴)))
3	1, 2	sylanb 581	1 ⊢ ((Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺) → ((𝐹 ∘ 𝐺)‘𝐴) = (𝐹‘(𝐺‘𝐴)))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  dom cdm 5619   ∘ ccom 5623  Fun wfun 6476   Fn wfn 6477  ‘cfv 6482

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 5235  ax-nul 5245  ax-pr 5371

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-fv 6490

This theorem is referenced by:  fin23lem30  10236  hashkf  14239  hashgval  14240  gsumpropd2lem  18553  ofco2  22336  opfv  32587  xppreima  32588  psgnfzto1stlem  33042  cycpmfv1  33055  cycpmfv2  33056  cyc3co2  33082  smatlem  33764  mdetpmtr1  33790  madjusmdetlem2  33795  madjusmdetlem4  33797  eulerpartlemgvv  34344  eulerpartlemgu  34345  sseqfv2  34362  reprpmtf1o  34594  hgt750lemg  34622  aks5lem2  42160  comptiunov2i  43679  choicefi  45178  fvcod  45205  evthiccabs  45477  cncficcgt0  45869  dvsinax  45894  fvvolioof  45970  fvvolicof  45972  stirlinglem14  46068  fourierdlem42  46130  hoicvr  46529  hoi2toco  46588  ovolval3  46628  ovolval4lem1  46630  ovnovollem1  46637  ovnovollem2  46638