Theorem fveq1d 5307

Description: Equality deduction for function value. (Contributed by NM, 2-Sep-2003.)

Hypothesis

Ref	Expression
fveq1d.1	|- ( ph -> F = G )

Assertion

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

Proof of Theorem fveq1d

Step	Hyp	Ref	Expression
1		fveq1d.1	. 2 |- ( ph -> F = G )
2		fveq1 5304	. 2 |- ( F = G -> ( F ` A ) = ( G ` A ) )
3	1, 2	syl 14	1 |- ( ph -> ( F ` A ) = ( G ` A ) )

Syntax hints:   -> wi 4   = wceq 1289   ` cfv 5015

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-rex 2365  df-uni 3654  df-br 3846  df-iota 4980  df-fv 5023

This theorem is referenced by:  fveq12d  5312  funssfv  5330  csbfv2g  5341  fvco4  5376  fvmptd  5385  fvmpt2d  5389  mpteqb  5393  fvmptt  5394  fmptco  5464  fvunsng  5491  fvsng  5493  fsnunfv  5498  f1ocnvfv1  5556  f1ocnvfv2  5557  fcof1  5562  fcofo  5563  fnofval  5865  offval2  5870  ofrfval2  5871  caofinvl  5877  tfrlemi1  6097  rdg0g  6153  freceq1  6157  oav  6215  omv  6216  oeiv  6217  mapxpen  6562  xpmapenlem  6563  exmidomni  6796  fseq1p1m1  9504  iseqeq3  9856  seq3shft2  9895  seq3f1olemqsum  9925  seq3f1olemstep  9926  seq3f1olemp  9927  ser3add  9931  iseqid  9935  iseqz  9939  ser0  9945  ser3le  9949  exp3val  9953  ibcval5  10167  bcn2  10168  iseqcoll  10243  shftcan1  10264  shftcan2  10265  shftvalg  10266  shftval4g  10267  climshft2  10691  sumeq2  10744  isummolem3  10766  isummo  10769  zisum  10770  fisum  10774  fsum3  10775  isumz  10777  fisumss  10780  fisumcvg2  10782  fsum3cvg2  10783  fsum3ser  10787  isumsplit  10881  fvsetsid  11523  setsidn  11539  setsnidn  11540  peano4nninf  11851