Theorem fveq1d 5674

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

Syntax hints:   -> wi 4   = wceq 1398   ` cfv 5354

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-uni 3917  df-br 4112  df-iota 5314  df-fv 5362

This theorem is referenced by:  fveq12d  5679  funssfv  5698  fv2prc  5711  csbfv2g  5713  fvco4  5751  fvmptd  5760  fvmpt2d  5766  mpteqb  5770  fvmptt  5771  fnmptfvd  5784  fmptco  5845  fvunsng  5880  fvsng  5882  fsnunfv  5887  f1ocnvfv1  5952  f1ocnvfv2  5953  fcof1  5958  fcofo  5959  ofvalg  6278  offval2  6284  ofrfval2  6285  caofinvl  6294  tfrlemi1  6565  rdg0g  6621  freceq1  6625  oav  6689  omv  6690  oeiv  6691  pw2f1odclem  7089  mapxpen  7103  xpmapenlem  7104  2omap  7271  nninfisollemne  7424  nninfisol  7426  exmidomni  7435  nninfwlpoimlemginf  7469  cc3  7584  fseq1p1m1  10432  seqeq3  10818  seq3f1olemqsum  10879  seq3f1olemstep  10880  seq3f1olemp  10881  seqf1oglem2  10886  seqf1og  10887  seq3id  10891  seq3z  10894  exp3val  10907  bcval5  11129  bcn2  11130  seq3coll  11218  s1fv  11318  ccat1st1st  11333  ccat2s1fvwd  11339  swrdfv  11349  pfxfv  11380  swrdswrd  11401  shftcan1  11523  shftcan2  11524  shftvalg  11525  shftval4g  11526  climshft2  11995  sumeq2  12048  summodc  12073  zsumdc  12074  fsum3  12077  isumz  12079  fisumss  12082  fsum3cvg2  12084  isumsplit  12181  prodeq2w  12246  prodeq2  12247  prodmodc  12268  zproddc  12269  fprodseq  12273  prod1dc  12276  fprodssdc  12280  nninfctlemfo  12740  odzval  12943  1arithlem2  13066  ballotfileme  13157  fvsetsid  13263  setsslid  13280  setsslnid  13281  prdsex  13499  prdsval  13503  prdsplusgfval  13514  prdsmulrfval  13516  imasival  13536  imasbas  13537  imasplusg  13538  imasmulr  13539  igsumvalx  13619  gsumfzval  13621  gsumpropd  13622  gsumress  13625  gsumval2  13627  grpinvval  13773  grpsubfvalg  13775  grpsubpropdg  13834  grpsubpropd2  13835  pwsinvg  13842  mulgfvalg  13855  mulgpropdg  13898  submmulg  13900  subgmulg  13922  releqgg  13954  eqgex  13955  eqgfval  13956  gsumfzmptfidmadd  14073  unitinvcl  14285  unitinvinv  14286  unitlinv  14288  unitrinv  14289  unitnegcl  14292  dvrfvald  14295  dvrvald  14296  rdivmuldivd  14306  subrgugrp  14402  rrgsupp  14428  lspval  14555  ixpsnbasval  14631  lidlnegcl  14650  rspcl  14656  rspssid  14657  rspssp  14659  rspsn  14699  zrhmulg  14785  znzrhval  14812  mplsubgfilemm  14870  mplsubgfilemcl  14871  mplsubgfileminv  14872  mplnegfi  14877  ntrval  14992  clsval  14993  neival  15025  cnpval  15080  txmetcnp  15400  metcnpd  15402  limccl  15541  ellimc3apf  15542  cnplimclemr  15551  limccnp2cntop  15559  dvfvalap  15563  dvfre  15592  plycoeid3  15639  plyrecj  15645  lgsval4  15910  lgsmod  15916  uhgrspansubgrlem  16288  vtxdgfval  16300  vtxdgfifival  16303  vtxdgop  16304  vtxdeqd  16308  vtxdfifiun  16309  1loopgrvd0fi  16318  1hevtxdg0fi  16319  1hevtxdg1en  16320  1hegrvtxdg1fi  16321  wksfval  16334  wlkres  16391  eupth2fi  16491  pw1map  16786  peano4nninf  16801  gsumgfsumlem  16882