Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvco2 Structured version   Visualization version   GIF version

Theorem fvco2 6739
 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.
StepHypRef Expression
1 fnsnfv 6724 . . . . . 6 ((𝐺 Fn 𝐴𝑋𝐴) → {(𝐺𝑋)} = (𝐺 “ {𝑋}))
21imaeq2d 5910 . . . . 5 ((𝐺 Fn 𝐴𝑋𝐴) → (𝐹 “ {(𝐺𝑋)}) = (𝐹 “ (𝐺 “ {𝑋})))
3 imaco 6085 . . . . 5 ((𝐹𝐺) “ {𝑋}) = (𝐹 “ (𝐺 “ {𝑋}))
42, 3syl6reqr 2878 . . . 4 ((𝐺 Fn 𝐴𝑋𝐴) → ((𝐹𝐺) “ {𝑋}) = (𝐹 “ {(𝐺𝑋)}))
54eleq2d 2901 . . 3 ((𝐺 Fn 𝐴𝑋𝐴) → (𝑥 ∈ ((𝐹𝐺) “ {𝑋}) ↔ 𝑥 ∈ (𝐹 “ {(𝐺𝑋)})))
65iotabidv 6320 . 2 ((𝐺 Fn 𝐴𝑋𝐴) → (℩𝑥𝑥 ∈ ((𝐹𝐺) “ {𝑋})) = (℩𝑥𝑥 ∈ (𝐹 “ {(𝐺𝑋)})))
7 dffv3 6647 . 2 ((𝐹𝐺)‘𝑋) = (℩𝑥𝑥 ∈ ((𝐹𝐺) “ {𝑋}))
8 dffv3 6647 . 2 (𝐹‘(𝐺𝑋)) = (℩𝑥𝑥 ∈ (𝐹 “ {(𝐺𝑋)}))
96, 7, 83eqtr4g 2884 1 ((𝐺 Fn 𝐴𝑋𝐴) → ((𝐹𝐺)‘𝑋) = (𝐹‘(𝐺𝑋)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2115  {csn 4548   “ cima 5539   ∘ ccom 5540  ℩cio 6293   Fn wfn 6331  ‘cfv 6336 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 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5184  ax-nul 5191  ax-pow 5247  ax-pr 5311 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3014  df-ral 3137  df-rex 3138  df-rab 3141  df-v 3481  df-sbc 3758  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-nul 4275  df-if 4449  df-sn 4549  df-pr 4551  df-op 4555  df-uni 4820  df-br 5048  df-opab 5110  df-id 5441  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6295  df-fun 6338  df-fn 6339  df-fv 6344 This theorem is referenced by:  fvco  6740  fvco3  6741  fvco4i  6743  fvcofneq  6840  ofco  7412  curry1  7782  curry2  7785  fsplitfpar  7797  enfixsn  8609  updjudhcoinlf  9345  updjudhcoinrg  9346  updjud  9347  smobeth  9993  fpwwe  10053  addpqnq  10345  mulpqnq  10348  revco  14185  ccatco  14186  cshco  14187  swrdco  14188  isoval  17024  prdsidlem  17932  gsumwmhm  17999  prdsinvlem  18197  gsmsymgrfixlem1  18544  f1omvdconj  18563  pmtrfinv  18578  symggen  18587  symgtrinv  18589  pmtr3ncomlem1  18590  ringidval  19242  prdsmgp  19349  lmhmco  19801  evlslem1  20281  evlsvar  20289  chrrhm  20664  cofipsgn  20723  dsmmbas2  20867  dsmm0cl  20870  frlmbas  20885  frlmup3  20930  frlmup4  20931  f1lindf  20952  lindfmm  20957  m1detdiag  21192  1stccnp  22056  prdstopn  22222  xpstopnlem2  22405  uniioombllem6  24181  ex-fpar  28236  0vfval  28378  cnre2csqlem  31171  mblfinlem2  34995  rabren3dioph  39588  hausgraph  39988  stoweidlem59  42543  afvco2  43574  isomushgr  44186  isomgrtrlem  44198  ackvalsucsucval  44932
 Copyright terms: Public domain W3C validator