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

Theorem fvco2 6168
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 6153 . . . . . 6 ((𝐺 Fn 𝐴𝑋𝐴) → {(𝐺𝑋)} = (𝐺 “ {𝑋}))
21imaeq2d 5372 . . . . 5 ((𝐺 Fn 𝐴𝑋𝐴) → (𝐹 “ {(𝐺𝑋)}) = (𝐹 “ (𝐺 “ {𝑋})))
3 imaco 5543 . . . . 5 ((𝐹𝐺) “ {𝑋}) = (𝐹 “ (𝐺 “ {𝑋}))
42, 3syl6reqr 2663 . . . 4 ((𝐺 Fn 𝐴𝑋𝐴) → ((𝐹𝐺) “ {𝑋}) = (𝐹 “ {(𝐺𝑋)}))
54eleq2d 2673 . . 3 ((𝐺 Fn 𝐴𝑋𝐴) → (𝑥 ∈ ((𝐹𝐺) “ {𝑋}) ↔ 𝑥 ∈ (𝐹 “ {(𝐺𝑋)})))
65iotabidv 5775 . 2 ((𝐺 Fn 𝐴𝑋𝐴) → (℩𝑥𝑥 ∈ ((𝐹𝐺) “ {𝑋})) = (℩𝑥𝑥 ∈ (𝐹 “ {(𝐺𝑋)})))
7 dffv3 6084 . 2 ((𝐹𝐺)‘𝑋) = (℩𝑥𝑥 ∈ ((𝐹𝐺) “ {𝑋}))
8 dffv3 6084 . 2 (𝐹‘(𝐺𝑋)) = (℩𝑥𝑥 ∈ (𝐹 “ {(𝐺𝑋)}))
96, 7, 83eqtr4g 2669 1 ((𝐺 Fn 𝐴𝑋𝐴) → ((𝐹𝐺)‘𝑋) = (𝐹‘(𝐺𝑋)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1475  wcel 1977  {csn 4125  cima 5031  ccom 5032  cio 5752   Fn wfn 5785  cfv 5790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4704  ax-nul 4712  ax-pow 4764  ax-pr 4828
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4368  df-br 4579  df-opab 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-fv 5798
This theorem is referenced by:  fvco  6169  fvco3  6170  fvco4i  6171  fvcofneq  6260  ofco  6793  curry1  7134  curry2  7137  enfixsn  7932  smobeth  9265  fpwwe  9325  addpqnq  9617  mulpqnq  9620  revco  13380  ccatco  13381  cshco  13382  swrdco  13383  isoval  16197  prdsidlem  17094  gsumwmhm  17154  prdsinvlem  17296  gsmsymgrfixlem1  17619  f1omvdconj  17638  pmtrfinv  17653  symggen  17662  symgtrinv  17664  pmtr3ncomlem1  17665  ringidval  18275  prdsmgp  18382  lmhmco  18813  evlslem1  19285  evlsvar  19293  chrrhm  19646  zrhcofipsgn  19706  dsmmbas2  19848  dsmm0cl  19851  frlmbas  19866  frlmup3  19906  frlmup4  19907  f1lindf  19928  lindfmm  19933  m1detdiag  20170  1stccnp  21023  prdstopn  21189  xpstopnlem2  21372  uniioombllem6  23107  0vfval  26639  cnre2csqlem  29078  mblfinlem2  32411  rabren3dioph  36191  hausgraph  36603  stoweidlem59  38746  afvco2  39700
  Copyright terms: Public domain W3C validator