Theorem fveq1d 5518

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 5515	. 2 |- ( F = G -> ( F ` A ) = ( G ` A ) )
3	1, 2	syl 14	1 |- ( ph -> ( F ` A ) = ( G ` A ) )

Syntax hints:   -> wi 4   = wceq 1353   ` cfv 5217

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-uni 3811  df-br 4005  df-iota 5179  df-fv 5225

This theorem is referenced by:  fveq12d  5523  funssfv  5542  csbfv2g  5553  fvco4  5589  fvmptd  5598  fvmpt2d  5603  mpteqb  5607  fvmptt  5608  fnmptfvd  5621  fmptco  5683  fvunsng  5711  fvsng  5713  fsnunfv  5718  f1ocnvfv1  5778  f1ocnvfv2  5779  fcof1  5784  fcofo  5785  ofvalg  6092  offval2  6098  ofrfval2  6099  caofinvl  6105  tfrlemi1  6333  rdg0g  6389  freceq1  6393  oav  6455  omv  6456  oeiv  6457  mapxpen  6848  xpmapenlem  6849  nninfisollemne  7129  nninfisol  7131  exmidomni  7140  nninfwlpoimlemginf  7174  cc3  7267  fseq1p1m1  10094  seqeq3  10450  seq3f1olemqsum  10500  seq3f1olemstep  10501  seq3f1olemp  10502  seq3id  10508  seq3z  10511  exp3val  10522  bcval5  10743  bcn2  10744  seq3coll  10822  shftcan1  10843  shftcan2  10844  shftvalg  10845  shftval4g  10846  climshft2  11314  sumeq2  11367  summodc  11391  zsumdc  11392  fsum3  11395  isumz  11397  fisumss  11400  fsum3cvg2  11402  isumsplit  11499  prodeq2w  11564  prodeq2  11565  prodmodc  11586  zproddc  11587  fprodseq  11591  prod1dc  11594  fprodssdc  11598  odzval  12241  1arithlem2  12362  fvsetsid  12496  setsslid  12513  setsslnid  12514  prdsex  12718  imasival  12727  imasbas  12728  imasplusg  12729  imasmulr  12730  grpinvval  12916  grpsubfvalg  12918  grpsubpropdg  12974  grpsubpropd2  12975  mulgfvalg  12985  mulgpropdg  13025  subgmulg  13048  releqgg  13080  eqgfval  13081  unitinvcl  13292  unitinvinv  13293  unitlinv  13295  unitrinv  13296  unitnegcl  13299  dvrfvald  13302  dvrvald  13303  rdivmuldivd  13313  subrgugrp  13361  ntrval  13613  clsval  13614  neival  13646  cnpval  13701  txmetcnp  14021  metcnpd  14023  limccl  14131  ellimc3apf  14132  cnplimclemr  14141  limccnp2cntop  14149  dvfvalap  14153  dvfre  14177  lgsval4  14424  lgsmod  14430  peano4nninf  14758