Theorem fvco2 6976

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 6247	. . . . 5 ⊢ ((𝐹 ∘ 𝐺) “ {𝑋}) = (𝐹 “ (𝐺 “ {𝑋}))
2		fnsnfv 6958	. . . . . 6 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → {(𝐺‘𝑋)} = (𝐺 “ {𝑋}))
3	2	imaeq2d 6056	. . . . 5 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝐹 “ {(𝐺‘𝑋)}) = (𝐹 “ (𝐺 “ {𝑋})))
4	1, 3	eqtr4id 2814	. . . 4 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺) “ {𝑋}) = (𝐹 “ {(𝐺‘𝑋)}))
5	4	eleq2d 2846	. . 3 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑥 ∈ ((𝐹 ∘ 𝐺) “ {𝑋}) ↔ 𝑥 ∈ (𝐹 “ {(𝐺‘𝑋)})))
6	5	iotabidv 6517	. 2 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (℩𝑥𝑥 ∈ ((𝐹 ∘ 𝐺) “ {𝑋})) = (℩𝑥𝑥 ∈ (𝐹 “ {(𝐺‘𝑋)})))
7		dffv3 6875	. 2 ⊢ ((𝐹 ∘ 𝐺)‘𝑋) = (℩𝑥𝑥 ∈ ((𝐹 ∘ 𝐺) “ {𝑋}))
8		dffv3 6875	. 2 ⊢ (𝐹‘(𝐺‘𝑋)) = (℩𝑥𝑥 ∈ (𝐹 “ {(𝐺‘𝑋)}))
9	6, 7, 8	3eqtr4g 2820	1 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝑋) = (𝐹‘(𝐺‘𝑋)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {csn 4584   “ cima 5658   ∘ ccom 5659  ℩cio 6487   Fn wfn 6528  ‘cfv 6533

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  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 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-fv 6541

This theorem is used by:  fvco  6977  fvco3  6979  fvco4i  6981  fvcofneq  7087  coof  7703  ofco  7704  curry1  8102  curry2  8105  fsplitfpar  8116  enfixsn  9085  updjudhcoinlf  9938  updjudhcoinrg  9939  updjud  9940  smobeth  10596  fpwwe  10656  addpqnq  10948  mulpqnq  10951  revco  14906  ccatco  14907  cshco  14908  swrdco  14909  isoval  17855  prdsidlem  18877  gsumwmhm  18955  prdsinvlem  19173  ghmquskerco  19412  gsmsymgrfixlem1  19555  f1omvdconj  19574  pmtrfinv  19589  symggen  19598  symgtrinv  19600  pmtr3ncomlem1  19601  prdsmgp  20285  ringidval  20323  lmhmco  21228  chrrhm  21745  cofipsgn  21807  dsmmbas2  21951  dsmm0cl  21954  frlmbas  21969  frlmup3  22014  frlmup4  22015  f1lindf  22036  lindfmm  22041  evlslem1  22299  evlsvar  22312  m1detdiag  22820  1stccnp  23689  prdstopn  23855  xpstopnlem2  24038  uniioombllem6  25817  precsexlem1  28473  precsexlem2  28474  precsexlem3  28475  precsexlem4  28476  precsexlem5  28477  ex-fpar  30943  0vfval  31088  cnre2csqlem  34421  mblfinlem2  38408  rabren3dioph  43657  hausgraph  44047  stoweidlem59  46888  afvco2  48065  gricushgr  48834  ackvalsucsucval  49619