Theorem fvco 6941

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  dom cdm 5631   ∘ ccom 5635  Fun wfun 6493   Fn wfn 6494  ‘cfv 6499

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-fv 6507

This theorem is referenced by:  fin23lem30  10271  hashkf  14273  hashgval  14274  gsumpropd2lem  18582  ofco2  22314  opfv  32541  xppreima  32542  psgnfzto1stlem  33030  cycpmfv1  33043  cycpmfv2  33044  cyc3co2  33070  smatlem  33760  mdetpmtr1  33786  madjusmdetlem2  33791  madjusmdetlem4  33793  eulerpartlemgvv  34340  eulerpartlemgu  34341  sseqfv2  34358  reprpmtf1o  34590  hgt750lemg  34618  aks5lem2  42148  comptiunov2i  43668  choicefi  45167  fvcod  45194  evthiccabs  45467  cncficcgt0  45859  dvsinax  45884  fvvolioof  45960  fvvolicof  45962  stirlinglem14  46058  fourierdlem42  46120  hoicvr  46519  hoi2toco  46578  ovolval3  46618  ovolval4lem1  46620  ovnovollem1  46627  ovnovollem2  46628