Theorem fveq1d 5572

Description: Equality deduction for function value. (Contributed by NM, 2-Sep-2003.)

Hypothesis

Ref	Expression
fveq1d.1	⊢ (𝜑 → 𝐹 = 𝐺)

Assertion

Ref	Expression
fveq1d	⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐴))

Proof of Theorem fveq1d

Step	Hyp	Ref	Expression
1		fveq1d.1	. 2 ⊢ (𝜑 → 𝐹 = 𝐺)
2		fveq1 5569	. 2 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1372  ‘cfv 5268

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-rex 2489  df-uni 3850  df-br 4044  df-iota 5229  df-fv 5276

This theorem is referenced by:  fveq12d  5577  funssfv  5596  fv2prc  5607  csbfv2g  5609  fvco4  5645  fvmptd  5654  fvmpt2d  5660  mpteqb  5664  fvmptt  5665  fnmptfvd  5678  fmptco  5740  fvunsng  5768  fvsng  5770  fsnunfv  5775  f1ocnvfv1  5836  f1ocnvfv2  5837  fcof1  5842  fcofo  5843  ofvalg  6158  offval2  6164  ofrfval2  6165  caofinvl  6174  tfrlemi1  6408  rdg0g  6464  freceq1  6468  oav  6530  omv  6531  oeiv  6532  pw2f1odclem  6913  mapxpen  6927  xpmapenlem  6928  nninfisollemne  7215  nninfisol  7217  exmidomni  7226  nninfwlpoimlemginf  7260  cc3  7362  fseq1p1m1  10198  seqeq3  10578  seq3f1olemqsum  10639  seq3f1olemstep  10640  seq3f1olemp  10641  seqf1oglem2  10646  seqf1og  10647  seq3id  10651  seq3z  10654  exp3val  10667  bcval5  10889  bcn2  10890  seq3coll  10968  shftcan1  11064  shftcan2  11065  shftvalg  11066  shftval4g  11067  climshft2  11536  sumeq2  11589  summodc  11613  zsumdc  11614  fsum3  11617  isumz  11619  fisumss  11622  fsum3cvg2  11624  isumsplit  11721  prodeq2w  11786  prodeq2  11787  prodmodc  11808  zproddc  11809  fprodseq  11813  prod1dc  11816  fprodssdc  11820  nninfctlemfo  12280  odzval  12483  1arithlem2  12606  fvsetsid  12785  setsslid  12802  setsslnid  12803  prdsex  13019  prdsval  13023  prdsplusgfval  13034  prdsmulrfval  13036  imasival  13056  imasbas  13057  imasplusg  13058  imasmulr  13059  igsumvalx  13139  gsumfzval  13141  gsumpropd  13142  gsumress  13145  gsumval2  13147  grpinvval  13293  grpsubfvalg  13295  grpsubpropdg  13354  grpsubpropd2  13355  pwsinvg  13362  mulgfvalg  13375  mulgpropdg  13418  submmulg  13420  subgmulg  13442  releqgg  13474  eqgex  13475  eqgfval  13476  gsumfzmptfidmadd  13593  unitinvcl  13803  unitinvinv  13804  unitlinv  13806  unitrinv  13807  unitnegcl  13810  dvrfvald  13813  dvrvald  13814  rdivmuldivd  13824  subrgugrp  13920  lspval  14070  ixpsnbasval  14146  lidlnegcl  14165  rspcl  14171  rspssid  14172  rspssp  14174  rspsn  14214  zrhmulg  14300  znzrhval  14327  mplsubgfilemm  14378  mplsubgfilemcl  14379  mplsubgfileminv  14380  mplnegfi  14385  ntrval  14500  clsval  14501  neival  14533  cnpval  14588  txmetcnp  14908  metcnpd  14910  limccl  15049  ellimc3apf  15050  cnplimclemr  15059  limccnp2cntop  15067  dvfvalap  15071  dvfre  15100  plycoeid3  15147  plyrecj  15153  lgsval4  15415  lgsmod  15421  2omap  15796  peano4nninf  15807