Theorem fveq12d 5583

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

Syntax hints:   -> wi 4   = wceq 1373   ` cfv 5271

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4045  df-iota 5232  df-fv 5279

This theorem is referenced by:  nffvd  5588  fvsng  5780  fvmpopr2d  6082  tfrlem3ag  6395  tfrlem3a  6396  tfrlemi1  6418  tfr1onlem3ag  6423  omp1eomlem  7196  lswwrd  11040  swrdval  11101  seq3shft  11149  climshft2  11617  fsum3  11698  ctiunctlemfo  12810  imasival  13138  gsumfzval  13223  gsumval2  13229  prdsinvlem  13440  mulgfvalg  13457  mulgval  13458  mulgnndir  13487  mulgpropdg  13500  unitinvinv  13886  rlmvalg  14216  rsp0  14255  znval  14398  reldvg  15151  dvfvalap  15153  lgsval  15481  lgsneg  15501