Theorem fveq1d 5650

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 5647	. 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 5333

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 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341

This theorem is referenced by:  fveq12d  5655  funssfv  5674  fv2prc  5687  csbfv2g  5689  fvco4  5727  fvmptd  5736  fvmpt2d  5742  mpteqb  5746  fvmptt  5747  fnmptfvd  5760  fmptco  5821  fvunsng  5856  fvsng  5858  fsnunfv  5863  f1ocnvfv1  5928  f1ocnvfv2  5929  fcof1  5934  fcofo  5935  ofvalg  6254  offval2  6260  ofrfval2  6261  caofinvl  6270  tfrlemi1  6541  rdg0g  6597  freceq1  6601  oav  6665  omv  6666  oeiv  6667  pw2f1odclem  7063  mapxpen  7077  xpmapenlem  7078  nninfisollemne  7390  nninfisol  7392  exmidomni  7401  nninfwlpoimlemginf  7435  cc3  7547  fseq1p1m1  10391  seqeq3  10777  seq3f1olemqsum  10838  seq3f1olemstep  10839  seq3f1olemp  10840  seqf1oglem2  10845  seqf1og  10846  seq3id  10850  seq3z  10853  exp3val  10866  bcval5  11088  bcn2  11089  seq3coll  11169  s1fv  11269  ccat1st1st  11284  ccat2s1fvwd  11290  swrdfv  11300  pfxfv  11331  swrdswrd  11352  shftcan1  11474  shftcan2  11475  shftvalg  11476  shftval4g  11477  climshft2  11946  sumeq2  11999  summodc  12024  zsumdc  12025  fsum3  12028  isumz  12030  fisumss  12033  fsum3cvg2  12035  isumsplit  12132  prodeq2w  12197  prodeq2  12198  prodmodc  12219  zproddc  12220  fprodseq  12224  prod1dc  12227  fprodssdc  12231  nninfctlemfo  12691  odzval  12894  1arithlem2  13017  fvsetsid  13196  setsslid  13213  setsslnid  13214  prdsex  13432  prdsval  13436  prdsplusgfval  13447  prdsmulrfval  13449  imasival  13469  imasbas  13470  imasplusg  13471  imasmulr  13472  igsumvalx  13552  gsumfzval  13554  gsumpropd  13555  gsumress  13558  gsumval2  13560  grpinvval  13706  grpsubfvalg  13708  grpsubpropdg  13767  grpsubpropd2  13768  pwsinvg  13775  mulgfvalg  13788  mulgpropdg  13831  submmulg  13833  subgmulg  13855  releqgg  13887  eqgex  13888  eqgfval  13889  gsumfzmptfidmadd  14006  unitinvcl  14218  unitinvinv  14219  unitlinv  14221  unitrinv  14222  unitnegcl  14225  dvrfvald  14228  dvrvald  14229  rdivmuldivd  14239  subrgugrp  14335  rrgsupp  14361  lspval  14486  ixpsnbasval  14562  lidlnegcl  14581  rspcl  14587  rspssid  14588  rspssp  14590  rspsn  14630  zrhmulg  14716  znzrhval  14743  mplsubgfilemm  14799  mplsubgfilemcl  14800  mplsubgfileminv  14801  mplnegfi  14806  ntrval  14921  clsval  14922  neival  14954  cnpval  15009  txmetcnp  15329  metcnpd  15331  limccl  15470  ellimc3apf  15471  cnplimclemr  15480  limccnp2cntop  15488  dvfvalap  15492  dvfre  15521  plycoeid3  15568  plyrecj  15574  lgsval4  15839  lgsmod  15845  uhgrspansubgrlem  16217  vtxdgfval  16229  vtxdgfifival  16232  vtxdgop  16233  vtxdeqd  16237  vtxdfifiun  16238  1loopgrvd0fi  16247  1hevtxdg0fi  16248  1hevtxdg1en  16249  1hegrvtxdg1fi  16250  wksfval  16263  wlkres  16320  eupth2fi  16420  2omap  16715  pw1map  16717  peano4nninf  16732  gsumgfsumlem  16812