Theorem fveq1d 5561

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

Syntax hints:   -> wi 4   = wceq 1364   ` cfv 5259

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267

This theorem is referenced by:  fveq12d  5566  funssfv  5585  fv2prc  5596  csbfv2g  5598  fvco4  5634  fvmptd  5643  fvmpt2d  5649  mpteqb  5653  fvmptt  5654  fnmptfvd  5667  fmptco  5729  fvunsng  5757  fvsng  5759  fsnunfv  5764  f1ocnvfv1  5825  f1ocnvfv2  5826  fcof1  5831  fcofo  5832  ofvalg  6147  offval2  6153  ofrfval2  6154  caofinvl  6162  tfrlemi1  6392  rdg0g  6448  freceq1  6452  oav  6514  omv  6515  oeiv  6516  pw2f1odclem  6897  mapxpen  6911  xpmapenlem  6912  nninfisollemne  7199  nninfisol  7201  exmidomni  7210  nninfwlpoimlemginf  7244  cc3  7338  fseq1p1m1  10172  seqeq3  10547  seq3f1olemqsum  10608  seq3f1olemstep  10609  seq3f1olemp  10610  seqf1oglem2  10615  seqf1og  10616  seq3id  10620  seq3z  10623  exp3val  10636  bcval5  10858  bcn2  10859  seq3coll  10937  shftcan1  11002  shftcan2  11003  shftvalg  11004  shftval4g  11005  climshft2  11474  sumeq2  11527  summodc  11551  zsumdc  11552  fsum3  11555  isumz  11557  fisumss  11560  fsum3cvg2  11562  isumsplit  11659  prodeq2w  11724  prodeq2  11725  prodmodc  11746  zproddc  11747  fprodseq  11751  prod1dc  11754  fprodssdc  11758  nninfctlemfo  12218  odzval  12421  1arithlem2  12544  fvsetsid  12723  setsslid  12740  setsslnid  12741  prdsex  12957  prdsval  12961  imasival  12975  imasbas  12976  imasplusg  12977  imasmulr  12978  igsumvalx  13058  gsumfzval  13060  gsumpropd  13061  gsumress  13064  gsumval2  13066  grpinvval  13201  grpsubfvalg  13203  grpsubpropdg  13262  grpsubpropd2  13263  mulgfvalg  13277  mulgpropdg  13320  submmulg  13322  subgmulg  13344  releqgg  13376  eqgex  13377  eqgfval  13378  gsumfzmptfidmadd  13495  unitinvcl  13705  unitinvinv  13706  unitlinv  13708  unitrinv  13709  unitnegcl  13712  dvrfvald  13715  dvrvald  13716  rdivmuldivd  13726  subrgugrp  13822  lspval  13972  ixpsnbasval  14048  lidlnegcl  14067  rspcl  14073  rspssid  14074  rspssp  14076  rspsn  14116  zrhmulg  14202  znzrhval  14229  ntrval  14372  clsval  14373  neival  14405  cnpval  14460  txmetcnp  14780  metcnpd  14782  limccl  14921  ellimc3apf  14922  cnplimclemr  14931  limccnp2cntop  14939  dvfvalap  14943  dvfre  14972  plycoeid3  15019  plyrecj  15025  lgsval4  15287  lgsmod  15293  peano4nninf  15677