Theorem fvco2 6940

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 6212	. . . . 5 ⊢ ((𝐹 ∘ 𝐺) “ {𝑋}) = (𝐹 “ (𝐺 “ {𝑋}))
2		fnsnfv 6922	. . . . . 6 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → {(𝐺‘𝑋)} = (𝐺 “ {𝑋}))
3	2	imaeq2d 6020	. . . . 5 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝐹 “ {(𝐺‘𝑋)}) = (𝐹 “ (𝐺 “ {𝑋})))
4	1, 3	eqtr4id 2783	. . . 4 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺) “ {𝑋}) = (𝐹 “ {(𝐺‘𝑋)}))
5	4	eleq2d 2814	. . 3 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑥 ∈ ((𝐹 ∘ 𝐺) “ {𝑋}) ↔ 𝑥 ∈ (𝐹 “ {(𝐺‘𝑋)})))
6	5	iotabidv 6483	. 2 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (℩𝑥𝑥 ∈ ((𝐹 ∘ 𝐺) “ {𝑋})) = (℩𝑥𝑥 ∈ (𝐹 “ {(𝐺‘𝑋)})))
7		dffv3 6836	. 2 ⊢ ((𝐹 ∘ 𝐺)‘𝑋) = (℩𝑥𝑥 ∈ ((𝐹 ∘ 𝐺) “ {𝑋}))
8		dffv3 6836	. 2 ⊢ (𝐹‘(𝐺‘𝑋)) = (℩𝑥𝑥 ∈ (𝐹 “ {(𝐺‘𝑋)}))
9	6, 7, 8	3eqtr4g 2789	1 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝑋) = (𝐹‘(𝐺‘𝑋)))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {csn 4585   “ cima 5634   ∘ ccom 5635  ℩cio 6450   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:  fvco  6941  fvco3  6942  fvco4i  6944  fvcofneq  7047  coof  7657  ofco  7658  curry1  8060  curry2  8063  fsplitfpar  8074  enfixsn  9027  updjudhcoinlf  9861  updjudhcoinrg  9862  updjud  9863  smobeth  10515  fpwwe  10575  addpqnq  10867  mulpqnq  10870  revco  14776  ccatco  14777  cshco  14778  swrdco  14779  isoval  17703  prdsidlem  18672  gsumwmhm  18748  prdsinvlem  18957  ghmquskerco  19192  gsmsymgrfixlem1  19333  f1omvdconj  19352  pmtrfinv  19367  symggen  19376  symgtrinv  19378  pmtr3ncomlem1  19379  prdsmgp  20036  ringidval  20068  lmhmco  20926  chrrhm  21417  cofipsgn  21478  dsmmbas2  21622  dsmm0cl  21625  frlmbas  21640  frlmup3  21685  frlmup4  21686  f1lindf  21707  lindfmm  21712  evlslem1  21965  evlsvar  21973  m1detdiag  22460  1stccnp  23325  prdstopn  23491  xpstopnlem2  23674  uniioombllem6  25465  precsexlem1  28085  precsexlem2  28086  precsexlem3  28087  precsexlem4  28088  precsexlem5  28089  ex-fpar  30364  0vfval  30508  cnre2csqlem  33873  mblfinlem2  37625  rabren3dioph  42776  hausgraph  43167  stoweidlem59  46030  afvco2  47150  gricushgr  47890  ackvalsucsucval  48650