Theorem fveq1d 5580

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

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

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-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-uni 3851  df-br 4046  df-iota 5233  df-fv 5280

This theorem is referenced by:  fveq12d  5585  funssfv  5604  fv2prc  5615  csbfv2g  5617  fvco4  5653  fvmptd  5662  fvmpt2d  5668  mpteqb  5672  fvmptt  5673  fnmptfvd  5686  fmptco  5748  fvunsng  5780  fvsng  5782  fsnunfv  5787  f1ocnvfv1  5848  f1ocnvfv2  5849  fcof1  5854  fcofo  5855  ofvalg  6170  offval2  6176  ofrfval2  6177  caofinvl  6186  tfrlemi1  6420  rdg0g  6476  freceq1  6480  oav  6542  omv  6543  oeiv  6544  pw2f1odclem  6933  mapxpen  6947  xpmapenlem  6948  nninfisollemne  7235  nninfisol  7237  exmidomni  7246  nninfwlpoimlemginf  7280  cc3  7382  fseq1p1m1  10218  seqeq3  10599  seq3f1olemqsum  10660  seq3f1olemstep  10661  seq3f1olemp  10662  seqf1oglem2  10667  seqf1og  10668  seq3id  10672  seq3z  10675  exp3val  10688  bcval5  10910  bcn2  10911  seq3coll  10989  s1fv  11083  ccat1st1st  11096  swrdfv  11109  pfxfv  11138  shftcan1  11178  shftcan2  11179  shftvalg  11180  shftval4g  11181  climshft2  11650  sumeq2  11703  summodc  11727  zsumdc  11728  fsum3  11731  isumz  11733  fisumss  11736  fsum3cvg2  11738  isumsplit  11835  prodeq2w  11900  prodeq2  11901  prodmodc  11922  zproddc  11923  fprodseq  11927  prod1dc  11930  fprodssdc  11934  nninfctlemfo  12394  odzval  12597  1arithlem2  12720  fvsetsid  12899  setsslid  12916  setsslnid  12917  prdsex  13134  prdsval  13138  prdsplusgfval  13149  prdsmulrfval  13151  imasival  13171  imasbas  13172  imasplusg  13173  imasmulr  13174  igsumvalx  13254  gsumfzval  13256  gsumpropd  13257  gsumress  13260  gsumval2  13262  grpinvval  13408  grpsubfvalg  13410  grpsubpropdg  13469  grpsubpropd2  13470  pwsinvg  13477  mulgfvalg  13490  mulgpropdg  13533  submmulg  13535  subgmulg  13557  releqgg  13589  eqgex  13590  eqgfval  13591  gsumfzmptfidmadd  13708  unitinvcl  13918  unitinvinv  13919  unitlinv  13921  unitrinv  13922  unitnegcl  13925  dvrfvald  13928  dvrvald  13929  rdivmuldivd  13939  subrgugrp  14035  lspval  14185  ixpsnbasval  14261  lidlnegcl  14280  rspcl  14286  rspssid  14287  rspssp  14289  rspsn  14329  zrhmulg  14415  znzrhval  14442  mplsubgfilemm  14493  mplsubgfilemcl  14494  mplsubgfileminv  14495  mplnegfi  14500  ntrval  14615  clsval  14616  neival  14648  cnpval  14703  txmetcnp  15023  metcnpd  15025  limccl  15164  ellimc3apf  15165  cnplimclemr  15174  limccnp2cntop  15182  dvfvalap  15186  dvfre  15215  plycoeid3  15262  plyrecj  15268  lgsval4  15530  lgsmod  15536  2omap  15969  peano4nninf  15980