Theorem fvco2 7013

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 6271	. . . . 5 ⊢ ((𝐹 ∘ 𝐺) “ {𝑋}) = (𝐹 “ (𝐺 “ {𝑋}))
2		fnsnfv 6995	. . . . . 6 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → {(𝐺‘𝑋)} = (𝐺 “ {𝑋}))
3	2	imaeq2d 6070	. . . . 5 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝐹 “ {(𝐺‘𝑋)}) = (𝐹 “ (𝐺 “ {𝑋})))
4	1, 3	eqtr4id 2817	. . . 4 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺) “ {𝑋}) = (𝐹 “ {(𝐺‘𝑋)}))
5	4	eleq2d 2850	. . 3 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑥 ∈ ((𝐹 ∘ 𝐺) “ {𝑋}) ↔ 𝑥 ∈ (𝐹 “ {(𝐺‘𝑋)})))
6	5	iotabidv 6549	. 2 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (℩𝑥𝑥 ∈ ((𝐹 ∘ 𝐺) “ {𝑋})) = (℩𝑥𝑥 ∈ (𝐹 “ {(𝐺‘𝑋)})))
7		dffv3 6912	. 2 ⊢ ((𝐹 ∘ 𝐺)‘𝑋) = (℩𝑥𝑥 ∈ ((𝐹 ∘ 𝐺) “ {𝑋}))
8		dffv3 6912	. 2 ⊢ (𝐹‘(𝐺‘𝑋)) = (℩𝑥𝑥 ∈ (𝐹 “ {(𝐺‘𝑋)}))
9	6, 7, 8	3eqtr4g 2823	1 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝑋) = (𝐹‘(𝐺‘𝑋)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  {csn 4588   “ cima 5661   ∘ ccom 5662  ℩cio 6518   Fn wfn 6561  ‘cfv 6566

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-fv 6574

This theorem is used by:  fvco  7014  fvco3  7016  fvco4i  7018  fvcofneq  7125  coof  7749  ofco  7750  curry1  8152  curry2  8155  fsplitfpar  8166  enfixsn  9143  updjudhcoinlf  10050  updjudhcoinrg  10051  updjud  10052  smobeth  10710  fpwwe  10770  addpqnq  11062  mulpqnq  11065  revco  15027  ccatco  15028  cshco  15029  swrdco  15030  isoval  17990  prdsidlem  19013  gsumwmhm  19091  prdsinvlem  19309  ghmquskerco  19549  gsmsymgrfixlem1  19692  f1omvdconj  19711  pmtrfinv  19726  symggen  19735  symgtrinv  19737  pmtr3ncomlem1  19738  prdsmgp  20422  ringidval  20460  lmhmco  21369  chrrhm  21892  cofipsgn  21954  dsmmbas2  22098  dsmm0cl  22101  frlmbas  22116  frlmup3  22161  frlmup4  22162  f1lindf  22183  lindfmm  22188  evlslem1  22446  evlsvar  22459  m1detdiag  22967  1stccnp  23836  prdstopn  24002  xpstopnlem2  24185  uniioombllem6  25964  precsexlem1  28650  precsexlem2  28651  precsexlem3  28652  precsexlem4  28653  precsexlem5  28654  ex-fpar  31120  0vfval  31265  cnre2csqlem  34653  mblfinlem2  38844  rabren3dioph  44088  hausgraph  44468  stoweidlem59  47342  afvco2  48519  gricushgr  49288  ackvalsucsucval  50131