Theorem fveq1d 5697

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 5694	. 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 5377

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 4131  df-iota 5337  df-fv 5385

This theorem is used by:  fveq12d  5702  funssfv  5721  fv2prc  5735  csbfv2g  5737  fvco4  5777  fvmptd  5786  fvmpt2d  5792  mpteqb  5796  fvmptt  5797  fnmptfvd  5813  fmptco  5874  fvunsng  5909  fvsng  5911  fsnunfv  5916  f1ocnvfv1  5983  f1ocnvfv2  5984  fcof1  5989  fcofo  5990  ofvalg  6312  offval2  6318  ofrfval2  6319  caofinvl  6328  tfrlemi1  6603  rdg0g  6659  freceq1  6663  oav  6727  omv  6728  oeiv  6729  pw2f1odclem  7134  mapxpen  7148  xpmapenlem  7149  2omap  7319  nninfisollemne  7472  nninfisol  7474  exmidomni  7483  nninfwlpoimlemginf  7517  cc3  7635  indval0  9300  fseq1p1m1  10512  seqeq3  10904  seq3f1olemqsum  10965  seq3f1olemstep  10966  seq3f1olemp  10967  seqf1oglem2  10972  seqf1og  10973  seq3id  10977  seq3z  10980  exp3val  10993  bcval5  11217  bcn2  11218  hashf1lem1  11301  seq3coll  11310  s1fv  11410  ccat1st1st  11425  ccat2s1fvwd  11431  swrdfv  11441  pfxfv  11472  swrdswrd  11493  shftcan1  11615  shftcan2  11616  shftvalg  11617  shftval4g  11618  climshft2  12091  sumeq2  12144  summodc  12169  zsumdc  12170  fsum3  12173  isumz  12175  fisumss  12178  fsum3cvg2  12180  isumsplit  12277  prodeq2w  12342  prodeq2  12343  prodmodc  12364  zproddc  12365  fprodseq  12369  prod1dc  12372  fprodssdc  12376  nninfctlemfo  12836  odzval  13043  1arithlem2  13166  ballotfileme  13288  ballotfilemi  13295  ballotfi  13334  fvsetsid  13438  setsslid  13455  setsslnid  13456  imasival  13680  imasbas  13681  imasplusg  13682  imasmulr  13683  gzsumvalx  13762  gzsumfzval  13764  gzsumress  13765  gzsumval2  13767  grpinvval  13901  grpsubfvalg  13903  grpsubpropdg  13962  grpsubpropd2  13963  mulgfvalg  13977  mulgpropdg  14020  submmulg  14022  subgmulg  14044  releqgg  14076  eqgex  14077  eqgfval  14078  gzsumshift  14233  prdsex  14256  prdsval  14257  prdsplusgfval  14268  prdsmulrfval  14270  pwsinvg  14299  unitinvcl  14514  unitinvinv  14515  unitlinv  14517  unitrinv  14518  unitnegcl  14521  dvrfvald  14524  dvrvald  14525  rdivmuldivd  14535  subrgugrp  14632  rrgsupp  14658  opprdrng  14704  lspval  14811  ixpsnbasval  14887  lidlnegcl  14906  rspcl  14912  rspssid  14913  rspssp  14915  rspsn  14955  zrhmulg  15039  znzrhval  15066  aspval  15099  mplsubgfilemm  15180  mplsubgfilemcl  15181  mplsubgfileminv  15182  mplnegfi  15187  ntrval  15302  clsval  15303  neival  15335  cnpval  15390  txmetcnp  15710  metcnpd  15712  limccl  15851  ellimc3apf  15852  cnplimclemr  15861  limccnp2cntop  15869  dvfvalap  15873  dvfre  15902  plycoeid3  15949  plyrecj  15955  lgsval4  16305  lgsmod  16311  uhgrspansubgrlem  16683  vtxdgfval  16695  vtxdgfifival  16698  vtxdgop  16699  vtxdeqd  16703  vtxdfifiun  16704  1loopgrvd0fi  16713  1hevtxdg0fi  16714  1hevtxdg1en  16715  1hegrvtxdg1fi  16716  wksfval  16729  wlkres  16786  eupth2fi  16886  pw1map  17191  peano4nninf  17215