Theorem fvco 6982

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  dom cdm 5659   ∘ ccom 5663  Fun wfun 6530   Fn wfn 6531  ‘cfv 6536

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 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

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 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6538  df-fn 6539  df-fv 6544

This theorem is referenced by:  fin23lem30  10361  hashkf  14355  hashgval  14356  gsumpropd2lem  18662  ofco2  22394  opfv  32627  xppreima  32628  psgnfzto1stlem  33116  cycpmfv1  33129  cycpmfv2  33130  cyc3co2  33156  smatlem  33833  mdetpmtr1  33859  madjusmdetlem2  33864  madjusmdetlem4  33866  eulerpartlemgvv  34413  eulerpartlemgu  34414  sseqfv2  34431  reprpmtf1o  34663  hgt750lemg  34691  aks5lem2  42205  comptiunov2i  43697  choicefi  45191  fvcod  45218  evthiccabs  45492  cncficcgt0  45884  dvsinax  45909  fvvolioof  45985  fvvolicof  45987  stirlinglem14  46083  fourierdlem42  46145  hoicvr  46544  hoi2toco  46603  ovolval3  46643  ovolval4lem1  46645  ovnovollem1  46652  ovnovollem2  46653