Theorem fveq12d 5682

Description: Equality deduction for function value. (Contributed by FL, 22-Dec-2008.)

Hypotheses

Ref	Expression
fveq12d.1	|- ( ph -> F = G )
fveq12d.2	|- ( ph -> A = B )

Assertion

Ref	Expression
fveq12d	|- ( ph -> ( F ` A ) = ( G ` B ) )

Proof of Theorem fveq12d

Step	Hyp	Ref	Expression
1		fveq12d.1	. . 3 |- ( ph -> F = G )
2	1	fveq1d 5677	. 2 |- ( ph -> ( F ` A ) = ( G ` A ) )
3		fveq12d.2	. . 3 |- ( ph -> A = B )
4	3	fveq2d 5679	. 2 |- ( ph -> ( G ` A ) = ( G ` B ) )
5	2, 4	eqtrd 2267	1 |- ( ph -> ( F ` A ) = ( G ` B ) )

Syntax hints:   -> wi 4   = wceq 1398   ` cfv 5357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365

This theorem is referenced by:  nffvd  5687  fvsng  5885  fvmpopr2d  6198  tfrlem3ag  6553  tfrlem3a  6554  tfrlemi1  6576  tfr1onlem3ag  6581  omp1eomlem  7398  lswwrd  11296  swrdval  11365  cats1fvnd  11482  seq3shft  11548  climshft2  12016  fsum3  12098  ctiunctlemfo  13274  imasival  13570  gsumfzval  13654  gsumval2  13660  mulgfvalg  13874  mulgval  13875  mulgnndir  13904  mulgpropdg  13917  prdsinvlem  14138  unitinvinv  14369  rlmvalg  14728  rsp0  14767  znval  14910  reldvg  15670  dvfvalap  15672  lgsval  16003  lgsneg  16023  wlkres  16500  depindlem1  16627  depindlem2  16628  depindlem3  16629