Theorem fvco2 6932

Description: Value of a function composition. Similar to second part of Theorem 3H of [Enderton] p. 47. (Contributed by NM, 9-Oct-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Revised by Stefan O'Rear, 16-Oct-2014.)

Assertion

Ref	Expression
fvco2	⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝑋) = (𝐹‘(𝐺‘𝑋)))

Proof of Theorem fvco2

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		imaco 6210	. . . . 5 ⊢ ((𝐹 ∘ 𝐺) “ {𝑋}) = (𝐹 “ (𝐺 “ {𝑋}))
2		fnsnfv 6914	. . . . . 6 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → {(𝐺‘𝑋)} = (𝐺 “ {𝑋}))
3	2	imaeq2d 6020	. . . . 5 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝐹 “ {(𝐺‘𝑋)}) = (𝐹 “ (𝐺 “ {𝑋})))
4	1, 3	eqtr4id 2791	. . . 4 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺) “ {𝑋}) = (𝐹 “ {(𝐺‘𝑋)}))
5	4	eleq2d 2823	. . 3 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑥 ∈ ((𝐹 ∘ 𝐺) “ {𝑋}) ↔ 𝑥 ∈ (𝐹 “ {(𝐺‘𝑋)})))
6	5	iotabidv 6477	. 2 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (℩𝑥𝑥 ∈ ((𝐹 ∘ 𝐺) “ {𝑋})) = (℩𝑥𝑥 ∈ (𝐹 “ {(𝐺‘𝑋)})))
7		dffv3 6831	. 2 ⊢ ((𝐹 ∘ 𝐺)‘𝑋) = (℩𝑥𝑥 ∈ ((𝐹 ∘ 𝐺) “ {𝑋}))
8		dffv3 6831	. 2 ⊢ (𝐹‘(𝐺‘𝑋)) = (℩𝑥𝑥 ∈ (𝐹 “ {(𝐺‘𝑋)}))
9	6, 7, 8	3eqtr4g 2797	1 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝑋) = (𝐹‘(𝐺‘𝑋)))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {csn 4568   “ cima 5628   ∘ ccom 5629  ℩cio 6447   Fn wfn 6488  ‘cfv 6493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-fv 6501

This theorem is referenced by:  fvco  6933  fvco3  6934  fvco4i  6936  fvcofneq  7040  coof  7649  ofco  7650  curry1  8048  curry2  8051  fsplitfpar  8062  enfixsn  9018  updjudhcoinlf  9850  updjudhcoinrg  9851  updjud  9852  smobeth  10503  fpwwe  10563  addpqnq  10855  mulpqnq  10858  revco  14790  ccatco  14791  cshco  14792  swrdco  14793  isoval  17726  prdsidlem  18731  gsumwmhm  18807  prdsinvlem  19019  ghmquskerco  19253  gsmsymgrfixlem1  19396  f1omvdconj  19415  pmtrfinv  19430  symggen  19439  symgtrinv  19441  pmtr3ncomlem1  19442  prdsmgp  20126  ringidval  20158  lmhmco  21033  chrrhm  21524  cofipsgn  21586  dsmmbas2  21730  dsmm0cl  21733  frlmbas  21748  frlmup3  21793  frlmup4  21794  f1lindf  21815  lindfmm  21820  evlslem1  22073  evlsvar  22086  m1detdiag  22575  1stccnp  23440  prdstopn  23606  xpstopnlem2  23789  uniioombllem6  25568  precsexlem1  28216  precsexlem2  28217  precsexlem3  28218  precsexlem4  28219  precsexlem5  28220  ex-fpar  30550  0vfval  30695  cnre2csqlem  34073  mblfinlem2  37996  rabren3dioph  43264  hausgraph  43654  stoweidlem59  46508  afvco2  47639  gricushgr  48408  ackvalsucsucval  49179