Theorem fvco 6983

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 6570	. 2 ⊢ (Fun 𝐺 ↔ 𝐺 Fn dom 𝐺)
2		fvco2 6982	. 2 ⊢ ((𝐺 Fn dom 𝐺 ∧ 𝐴 ∈ dom 𝐺) → ((𝐹 ∘ 𝐺)‘𝐴) = (𝐹‘(𝐺‘𝐴)))
3	1, 2	sylanb 593	1 ⊢ ((Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺) → ((𝐹 ∘ 𝐺)‘𝐴) = (𝐹‘(𝐺‘𝐴)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  dom cdm 5651   ∘ ccom 5655  Fun wfun 6532   Fn wfn 6533  ‘cfv 6538

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 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6494  df-fun 6540  df-fn 6541  df-fv 6546

This theorem is used by:  fvcod  6984  fin23lem30  10420  hashkf  14476  hashgval  14477  gsumpropd2lem  18868  ofco2  22766  opfv  33238  xppreima  33239  psgnfzto1stlem  33661  cycpmfv1  33674  cycpmfv2  33675  cyc3co2  33701  smatlem  34429  mdetpmtr1  34455  madjusmdetlem2  34460  madjusmdetlem4  34462  eulerpartlemgvv  35008  eulerpartlemgu  35009  sseqfv2  35026  reprpmtf1o  35255  hgt750lemg  35283  aks5lem2  43237  comptiunov2i  44705  choicefi  46213  evthiccabs  46507  cncficcgt0  46897  dvsinax  46922  fvvolioof  46998  fvvolicof  47000  stirlinglem14  47096  fourierdlem42  47158  hoicvr  47557  hoi2toco  47616  ovolval3  47656  ovolval4lem1  47658  ovnovollem1  47665  ovnovollem2  47666