Theorem fveq12d 5633

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 5628	. 2 |- ( ph -> ( F ` A ) = ( G ` A ) )
3		fveq12d.2	. . 3 |- ( ph -> A = B )
4	3	fveq2d 5630	. 2 |- ( ph -> ( G ` A ) = ( G ` B ) )
5	2, 4	eqtrd 2262	1 |- ( ph -> ( F ` A ) = ( G ` B ) )

Syntax hints:   -> wi 4   = wceq 1395   ` cfv 5317

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-br 4083  df-iota 5277  df-fv 5325

This theorem is referenced by:  nffvd  5638  fvsng  5834  fvmpopr2d  6140  tfrlem3ag  6453  tfrlem3a  6454  tfrlemi1  6476  tfr1onlem3ag  6481  omp1eomlem  7257  lswwrd  11113  swrdval  11175  cats1fvnd  11292  seq3shft  11344  climshft2  11812  fsum3  11893  ctiunctlemfo  13005  imasival  13334  gsumfzval  13419  gsumval2  13425  prdsinvlem  13636  mulgfvalg  13653  mulgval  13654  mulgnndir  13683  mulgpropdg  13696  unitinvinv  14082  rlmvalg  14412  rsp0  14451  znval  14594  reldvg  15347  dvfvalap  15349  lgsval  15677  lgsneg  15697