Theorem fveq1d 5532

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

Syntax hints:   -> wi 4   = wceq 1364   ` cfv 5231

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rex 2474  df-uni 3825  df-br 4019  df-iota 5193  df-fv 5239

This theorem is referenced by:  fveq12d  5537  funssfv  5556  fv2prc  5566  csbfv2g  5568  fvco4  5604  fvmptd  5613  fvmpt2d  5618  mpteqb  5622  fvmptt  5623  fnmptfvd  5636  fmptco  5698  fvunsng  5726  fvsng  5728  fsnunfv  5733  f1ocnvfv1  5794  f1ocnvfv2  5795  fcof1  5800  fcofo  5801  ofvalg  6110  offval2  6116  ofrfval2  6117  caofinvl  6123  tfrlemi1  6351  rdg0g  6407  freceq1  6411  oav  6473  omv  6474  oeiv  6475  mapxpen  6866  xpmapenlem  6867  nninfisollemne  7147  nninfisol  7149  exmidomni  7158  nninfwlpoimlemginf  7192  cc3  7285  fseq1p1m1  10112  seqeq3  10468  seq3f1olemqsum  10518  seq3f1olemstep  10519  seq3f1olemp  10520  seq3id  10526  seq3z  10529  exp3val  10540  bcval5  10761  bcn2  10762  seq3coll  10840  shftcan1  10861  shftcan2  10862  shftvalg  10863  shftval4g  10864  climshft2  11332  sumeq2  11385  summodc  11409  zsumdc  11410  fsum3  11413  isumz  11415  fisumss  11418  fsum3cvg2  11420  isumsplit  11517  prodeq2w  11582  prodeq2  11583  prodmodc  11604  zproddc  11605  fprodseq  11609  prod1dc  11612  fprodssdc  11616  odzval  12259  1arithlem2  12380  fvsetsid  12514  setsslid  12531  setsslnid  12532  prdsex  12740  imasival  12749  imasbas  12750  imasplusg  12751  imasmulr  12752  grpinvval  12953  grpsubfvalg  12955  grpsubpropdg  13014  grpsubpropd2  13015  mulgfvalg  13029  mulgpropdg  13070  subgmulg  13093  releqgg  13125  eqgex  13126  eqgfval  13127  unitinvcl  13434  unitinvinv  13435  unitlinv  13437  unitrinv  13438  unitnegcl  13441  dvrfvald  13444  dvrvald  13445  rdivmuldivd  13455  subrgugrp  13548  lspval  13667  ixpsnbasval  13743  lidlnegcl  13762  rspcl  13768  rspssid  13769  rspssp  13771  zrhmulg  13878  ntrval  14007  clsval  14008  neival  14040  cnpval  14095  txmetcnp  14415  metcnpd  14417  limccl  14525  ellimc3apf  14526  cnplimclemr  14535  limccnp2cntop  14543  dvfvalap  14547  dvfre  14571  lgsval4  14818  lgsmod  14824  peano4nninf  15153