Theorem fveq1d 5700

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   ` cfv 5380

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-uni 3936  df-br 4132  df-iota 5340  df-fv 5388

This theorem is used by:  fveq12d  5705  funssfv  5724  fv2prc  5738  csbfv2g  5740  fvco4  5780  fvmptd  5789  fvmpt2d  5795  mpteqb  5799  fvmptt  5800  fnmptfvd  5816  fmptco  5877  fvunsng  5912  fvsng  5914  fsnunfv  5919  f1ocnvfv1  5986  f1ocnvfv2  5987  fcof1  5992  fcofo  5993  ofvalg  6316  offval2  6322  ofrfval2  6323  caofinvl  6332  tfrlemi1  6607  rdg0g  6663  freceq1  6667  oav  6731  omv  6732  oeiv  6733  pw2f1odclem  7138  mapxpen  7152  xpmapenlem  7153  2omap  7324  nninfisollemne  7477  nninfisol  7479  exmidomni  7488  nninfwlpoimlemginf  7522  cc3  7640  indval0  9306  fseq1p1m1  10518  seqeq3  10910  seq3f1olemqsum  10971  seq3f1olemstep  10972  seq3f1olemp  10973  seqf1oglem2  10978  seqf1og  10979  seq3id  10983  seq3z  10986  exp3val  10999  bcval5  11223  bcn2  11224  hashf1lem1  11307  seq3coll  11316  s1fv  11416  ccat1st1st  11431  ccat2s1fvwd  11437  swrdfv  11447  pfxfv  11478  swrdswrd  11499  shftcan1  11621  shftcan2  11622  shftvalg  11623  shftval4g  11624  climshft2  12097  sumeq2  12150  summodc  12175  zsumdc  12176  fsum3  12179  isumz  12181  fisumss  12184  fsum3cvg2  12186  isumsplit  12283  prodeq2w  12348  prodeq2  12349  prodmodc  12370  zproddc  12371  fprodseq  12375  prod1dc  12378  fprodssdc  12382  nninfctlemfo  12842  odzval  13049  1arithlem2  13172  ballotfileme  13294  ballotfilemi  13301  ballotfi  13340  fvsetsid  13444  setsslid  13461  setsslnid  13462  imasival  13686  imasbas  13687  imasplusg  13688  imasmulr  13689  gzsumvalx  13768  gzsumfzval  13770  gzsumress  13771  gzsumval2  13773  grpinvval  13907  grpsubfvalg  13909  grpsubpropdg  13968  grpsubpropd2  13969  mulgfvalg  13983  mulgpropdg  14026  submmulg  14028  subgmulg  14050  releqgg  14082  eqgex  14083  eqgfval  14084  gzsumshift  14239  prdsex  14279  prdsval  14280  prdsplusgfval  14291  prdsmulrfval  14293  pwsinvg  14322  unitinvcl  14539  unitinvinv  14540  unitlinv  14542  unitrinv  14543  unitnegcl  14546  dvrfvald  14549  dvrvald  14550  rdivmuldivd  14560  subrgugrp  14657  rrgsupp  14683  opprdrng  14729  lspval  14836  ixpsnbasval  14912  lidlnegcl  14931  rspcl  14937  rspssid  14938  rspssp  14940  rspsn  14980  zrhmulg  15064  znzrhval  15091  aspval  15124  psrdifi  15202  psrdirfi  15203  mplsubgfilemm  15214  mplsubgfilemcl  15215  mplsubgfileminv  15216  mplnegfi  15221  ntrval  15336  clsval  15337  neival  15369  cnpval  15424  txmetcnp  15744  metcnpd  15746  limccl  15885  ellimc3apf  15886  cnplimclemr  15895  limccnp2cntop  15903  dvfvalap  15907  dvfre  15936  plycoeid3  15983  plyrecj  15989  lgsval4  16344  lgsmod  16350  uhgrspansubgrlem  16722  vtxdgfval  16734  vtxdgfifival  16737  vtxdgop  16738  vtxdeqd  16742  vtxdfifiun  16743  1loopgrvd0fi  16752  1hevtxdg0fi  16753  1hevtxdg1en  16754  1hegrvtxdg1fi  16755  wksfval  16768  wlkres  16825  eupth2fi  16925  pw1map  17230  peano4nninf  17255