Theorem fveq1d 5601

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 5598	. 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 5290

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rex 2492  df-uni 3865  df-br 4060  df-iota 5251  df-fv 5298

This theorem is referenced by:  fveq12d  5606  funssfv  5625  fv2prc  5636  csbfv2g  5638  fvco4  5674  fvmptd  5683  fvmpt2d  5689  mpteqb  5693  fvmptt  5694  fnmptfvd  5707  fmptco  5769  fvunsng  5801  fvsng  5803  fsnunfv  5808  f1ocnvfv1  5869  f1ocnvfv2  5870  fcof1  5875  fcofo  5876  ofvalg  6191  offval2  6197  ofrfval2  6198  caofinvl  6207  tfrlemi1  6441  rdg0g  6497  freceq1  6501  oav  6563  omv  6564  oeiv  6565  pw2f1odclem  6956  mapxpen  6970  xpmapenlem  6971  nninfisollemne  7259  nninfisol  7261  exmidomni  7270  nninfwlpoimlemginf  7304  cc3  7415  fseq1p1m1  10251  seqeq3  10634  seq3f1olemqsum  10695  seq3f1olemstep  10696  seq3f1olemp  10697  seqf1oglem2  10702  seqf1og  10703  seq3id  10707  seq3z  10710  exp3val  10723  bcval5  10945  bcn2  10946  seq3coll  11024  s1fv  11118  ccat1st1st  11131  swrdfv  11144  pfxfv  11175  swrdswrd  11196  shftcan1  11260  shftcan2  11261  shftvalg  11262  shftval4g  11263  climshft2  11732  sumeq2  11785  summodc  11809  zsumdc  11810  fsum3  11813  isumz  11815  fisumss  11818  fsum3cvg2  11820  isumsplit  11917  prodeq2w  11982  prodeq2  11983  prodmodc  12004  zproddc  12005  fprodseq  12009  prod1dc  12012  fprodssdc  12016  nninfctlemfo  12476  odzval  12679  1arithlem2  12802  fvsetsid  12981  setsslid  12998  setsslnid  12999  prdsex  13216  prdsval  13220  prdsplusgfval  13231  prdsmulrfval  13233  imasival  13253  imasbas  13254  imasplusg  13255  imasmulr  13256  igsumvalx  13336  gsumfzval  13338  gsumpropd  13339  gsumress  13342  gsumval2  13344  grpinvval  13490  grpsubfvalg  13492  grpsubpropdg  13551  grpsubpropd2  13552  pwsinvg  13559  mulgfvalg  13572  mulgpropdg  13615  submmulg  13617  subgmulg  13639  releqgg  13671  eqgex  13672  eqgfval  13673  gsumfzmptfidmadd  13790  unitinvcl  14000  unitinvinv  14001  unitlinv  14003  unitrinv  14004  unitnegcl  14007  dvrfvald  14010  dvrvald  14011  rdivmuldivd  14021  subrgugrp  14117  lspval  14267  ixpsnbasval  14343  lidlnegcl  14362  rspcl  14368  rspssid  14369  rspssp  14371  rspsn  14411  zrhmulg  14497  znzrhval  14524  mplsubgfilemm  14575  mplsubgfilemcl  14576  mplsubgfileminv  14577  mplnegfi  14582  ntrval  14697  clsval  14698  neival  14730  cnpval  14785  txmetcnp  15105  metcnpd  15107  limccl  15246  ellimc3apf  15247  cnplimclemr  15256  limccnp2cntop  15264  dvfvalap  15268  dvfre  15297  plycoeid3  15344  plyrecj  15350  lgsval4  15612  lgsmod  15618  2omap  16132  pw1map  16134  peano4nninf  16145