Theorem fveq1d 5578

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

Syntax hints:   -> wi 4   = wceq 1373   ` cfv 5271

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-uni 3851  df-br 4045  df-iota 5232  df-fv 5279

This theorem is referenced by:  fveq12d  5583  funssfv  5602  fv2prc  5613  csbfv2g  5615  fvco4  5651  fvmptd  5660  fvmpt2d  5666  mpteqb  5670  fvmptt  5671  fnmptfvd  5684  fmptco  5746  fvunsng  5778  fvsng  5780  fsnunfv  5785  f1ocnvfv1  5846  f1ocnvfv2  5847  fcof1  5852  fcofo  5853  ofvalg  6168  offval2  6174  ofrfval2  6175  caofinvl  6184  tfrlemi1  6418  rdg0g  6474  freceq1  6478  oav  6540  omv  6541  oeiv  6542  pw2f1odclem  6931  mapxpen  6945  xpmapenlem  6946  nninfisollemne  7233  nninfisol  7235  exmidomni  7244  nninfwlpoimlemginf  7278  cc3  7380  fseq1p1m1  10216  seqeq3  10597  seq3f1olemqsum  10658  seq3f1olemstep  10659  seq3f1olemp  10660  seqf1oglem2  10665  seqf1og  10666  seq3id  10670  seq3z  10673  exp3val  10686  bcval5  10908  bcn2  10909  seq3coll  10987  s1fv  11080  ccat1st1st  11093  swrdfv  11106  shftcan1  11145  shftcan2  11146  shftvalg  11147  shftval4g  11148  climshft2  11617  sumeq2  11670  summodc  11694  zsumdc  11695  fsum3  11698  isumz  11700  fisumss  11703  fsum3cvg2  11705  isumsplit  11802  prodeq2w  11867  prodeq2  11868  prodmodc  11889  zproddc  11890  fprodseq  11894  prod1dc  11897  fprodssdc  11901  nninfctlemfo  12361  odzval  12564  1arithlem2  12687  fvsetsid  12866  setsslid  12883  setsslnid  12884  prdsex  13101  prdsval  13105  prdsplusgfval  13116  prdsmulrfval  13118  imasival  13138  imasbas  13139  imasplusg  13140  imasmulr  13141  igsumvalx  13221  gsumfzval  13223  gsumpropd  13224  gsumress  13227  gsumval2  13229  grpinvval  13375  grpsubfvalg  13377  grpsubpropdg  13436  grpsubpropd2  13437  pwsinvg  13444  mulgfvalg  13457  mulgpropdg  13500  submmulg  13502  subgmulg  13524  releqgg  13556  eqgex  13557  eqgfval  13558  gsumfzmptfidmadd  13675  unitinvcl  13885  unitinvinv  13886  unitlinv  13888  unitrinv  13889  unitnegcl  13892  dvrfvald  13895  dvrvald  13896  rdivmuldivd  13906  subrgugrp  14002  lspval  14152  ixpsnbasval  14228  lidlnegcl  14247  rspcl  14253  rspssid  14254  rspssp  14256  rspsn  14296  zrhmulg  14382  znzrhval  14409  mplsubgfilemm  14460  mplsubgfilemcl  14461  mplsubgfileminv  14462  mplnegfi  14467  ntrval  14582  clsval  14583  neival  14615  cnpval  14670  txmetcnp  14990  metcnpd  14992  limccl  15131  ellimc3apf  15132  cnplimclemr  15141  limccnp2cntop  15149  dvfvalap  15153  dvfre  15182  plycoeid3  15229  plyrecj  15235  lgsval4  15497  lgsmod  15503  2omap  15932  peano4nninf  15943