Theorem fveq1d 5563

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 5560	. 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  5568  funssfv  5587  fv2prc  5598  csbfv2g  5600  fvco4  5636  fvmptd  5645  fvmpt2d  5651  mpteqb  5655  fvmptt  5656  fnmptfvd  5669  fmptco  5731  fvunsng  5759  fvsng  5761  fsnunfv  5766  f1ocnvfv1  5827  f1ocnvfv2  5828  fcof1  5833  fcofo  5834  ofvalg  6149  offval2  6155  ofrfval2  6156  caofinvl  6165  tfrlemi1  6399  rdg0g  6455  freceq1  6459  oav  6521  omv  6522  oeiv  6523  pw2f1odclem  6904  mapxpen  6918  xpmapenlem  6919  nninfisollemne  7206  nninfisol  7208  exmidomni  7217  nninfwlpoimlemginf  7251  cc3  7351  fseq1p1m1  10186  seqeq3  10561  seq3f1olemqsum  10622  seq3f1olemstep  10623  seq3f1olemp  10624  seqf1oglem2  10629  seqf1og  10630  seq3id  10634  seq3z  10637  exp3val  10650  bcval5  10872  bcn2  10873  seq3coll  10951  shftcan1  11016  shftcan2  11017  shftvalg  11018  shftval4g  11019  climshft2  11488  sumeq2  11541  summodc  11565  zsumdc  11566  fsum3  11569  isumz  11571  fisumss  11574  fsum3cvg2  11576  isumsplit  11673  prodeq2w  11738  prodeq2  11739  prodmodc  11760  zproddc  11761  fprodseq  11765  prod1dc  11768  fprodssdc  11772  nninfctlemfo  12232  odzval  12435  1arithlem2  12558  fvsetsid  12737  setsslid  12754  setsslnid  12755  prdsex  12971  prdsval  12975  prdsplusgfval  12986  prdsmulrfval  12988  imasival  13008  imasbas  13009  imasplusg  13010  imasmulr  13011  igsumvalx  13091  gsumfzval  13093  gsumpropd  13094  gsumress  13097  gsumval2  13099  grpinvval  13245  grpsubfvalg  13247  grpsubpropdg  13306  grpsubpropd2  13307  pwsinvg  13314  mulgfvalg  13327  mulgpropdg  13370  submmulg  13372  subgmulg  13394  releqgg  13426  eqgex  13427  eqgfval  13428  gsumfzmptfidmadd  13545  unitinvcl  13755  unitinvinv  13756  unitlinv  13758  unitrinv  13759  unitnegcl  13762  dvrfvald  13765  dvrvald  13766  rdivmuldivd  13776  subrgugrp  13872  lspval  14022  ixpsnbasval  14098  lidlnegcl  14117  rspcl  14123  rspssid  14124  rspssp  14126  rspsn  14166  zrhmulg  14252  znzrhval  14279  ntrval  14430  clsval  14431  neival  14463  cnpval  14518  txmetcnp  14838  metcnpd  14840  limccl  14979  ellimc3apf  14980  cnplimclemr  14989  limccnp2cntop  14997  dvfvalap  15001  dvfre  15030  plycoeid3  15077  plyrecj  15083  lgsval4  15345  lgsmod  15351  2omap  15726  peano4nninf  15737