Theorem fveq1d 5556

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 5553	. 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 5254

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-uni 3836  df-br 4030  df-iota 5215  df-fv 5262

This theorem is referenced by:  fveq12d  5561  funssfv  5580  fv2prc  5591  csbfv2g  5593  fvco4  5629  fvmptd  5638  fvmpt2d  5644  mpteqb  5648  fvmptt  5649  fnmptfvd  5662  fmptco  5724  fvunsng  5752  fvsng  5754  fsnunfv  5759  f1ocnvfv1  5820  f1ocnvfv2  5821  fcof1  5826  fcofo  5827  ofvalg  6140  offval2  6146  ofrfval2  6147  caofinvl  6155  tfrlemi1  6385  rdg0g  6441  freceq1  6445  oav  6507  omv  6508  oeiv  6509  pw2f1odclem  6890  mapxpen  6904  xpmapenlem  6905  nninfisollemne  7190  nninfisol  7192  exmidomni  7201  nninfwlpoimlemginf  7235  cc3  7328  fseq1p1m1  10160  seqeq3  10523  seq3f1olemqsum  10584  seq3f1olemstep  10585  seq3f1olemp  10586  seqf1oglem2  10591  seqf1og  10592  seq3id  10596  seq3z  10599  exp3val  10612  bcval5  10834  bcn2  10835  seq3coll  10913  shftcan1  10978  shftcan2  10979  shftvalg  10980  shftval4g  10981  climshft2  11449  sumeq2  11502  summodc  11526  zsumdc  11527  fsum3  11530  isumz  11532  fisumss  11535  fsum3cvg2  11537  isumsplit  11634  prodeq2w  11699  prodeq2  11700  prodmodc  11721  zproddc  11722  fprodseq  11726  prod1dc  11729  fprodssdc  11733  nninfctlemfo  12177  odzval  12379  1arithlem2  12502  fvsetsid  12652  setsslid  12669  setsslnid  12670  prdsex  12880  imasival  12889  imasbas  12890  imasplusg  12891  imasmulr  12892  igsumvalx  12972  gsumfzval  12974  gsumpropd  12975  gsumress  12978  gsumval2  12980  grpinvval  13115  grpsubfvalg  13117  grpsubpropdg  13176  grpsubpropd2  13177  mulgfvalg  13191  mulgpropdg  13234  submmulg  13236  subgmulg  13258  releqgg  13290  eqgex  13291  eqgfval  13292  gsumfzmptfidmadd  13409  unitinvcl  13619  unitinvinv  13620  unitlinv  13622  unitrinv  13623  unitnegcl  13626  dvrfvald  13629  dvrvald  13630  rdivmuldivd  13640  subrgugrp  13736  lspval  13886  ixpsnbasval  13962  lidlnegcl  13981  rspcl  13987  rspssid  13988  rspssp  13990  rspsn  14030  zrhmulg  14108  znzrhval  14135  ntrval  14278  clsval  14279  neival  14311  cnpval  14366  txmetcnp  14686  metcnpd  14688  limccl  14813  ellimc3apf  14814  cnplimclemr  14823  limccnp2cntop  14831  dvfvalap  14835  dvfre  14859  lgsval4  15136  lgsmod  15142  peano4nninf  15496