Theorem fveq1d 5591

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 5588	. 2 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1373  ‘cfv 5280

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 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rex 2491  df-uni 3857  df-br 4052  df-iota 5241  df-fv 5288

This theorem is referenced by:  fveq12d  5596  funssfv  5615  fv2prc  5626  csbfv2g  5628  fvco4  5664  fvmptd  5673  fvmpt2d  5679  mpteqb  5683  fvmptt  5684  fnmptfvd  5697  fmptco  5759  fvunsng  5791  fvsng  5793  fsnunfv  5798  f1ocnvfv1  5859  f1ocnvfv2  5860  fcof1  5865  fcofo  5866  ofvalg  6181  offval2  6187  ofrfval2  6188  caofinvl  6197  tfrlemi1  6431  rdg0g  6487  freceq1  6491  oav  6553  omv  6554  oeiv  6555  pw2f1odclem  6946  mapxpen  6960  xpmapenlem  6961  nninfisollemne  7248  nninfisol  7250  exmidomni  7259  nninfwlpoimlemginf  7293  cc3  7400  fseq1p1m1  10236  seqeq3  10619  seq3f1olemqsum  10680  seq3f1olemstep  10681  seq3f1olemp  10682  seqf1oglem2  10687  seqf1og  10688  seq3id  10692  seq3z  10695  exp3val  10708  bcval5  10930  bcn2  10931  seq3coll  11009  s1fv  11103  ccat1st1st  11116  swrdfv  11129  pfxfv  11160  swrdswrd  11181  shftcan1  11220  shftcan2  11221  shftvalg  11222  shftval4g  11223  climshft2  11692  sumeq2  11745  summodc  11769  zsumdc  11770  fsum3  11773  isumz  11775  fisumss  11778  fsum3cvg2  11780  isumsplit  11877  prodeq2w  11942  prodeq2  11943  prodmodc  11964  zproddc  11965  fprodseq  11969  prod1dc  11972  fprodssdc  11976  nninfctlemfo  12436  odzval  12639  1arithlem2  12762  fvsetsid  12941  setsslid  12958  setsslnid  12959  prdsex  13176  prdsval  13180  prdsplusgfval  13191  prdsmulrfval  13193  imasival  13213  imasbas  13214  imasplusg  13215  imasmulr  13216  igsumvalx  13296  gsumfzval  13298  gsumpropd  13299  gsumress  13302  gsumval2  13304  grpinvval  13450  grpsubfvalg  13452  grpsubpropdg  13511  grpsubpropd2  13512  pwsinvg  13519  mulgfvalg  13532  mulgpropdg  13575  submmulg  13577  subgmulg  13599  releqgg  13631  eqgex  13632  eqgfval  13633  gsumfzmptfidmadd  13750  unitinvcl  13960  unitinvinv  13961  unitlinv  13963  unitrinv  13964  unitnegcl  13967  dvrfvald  13970  dvrvald  13971  rdivmuldivd  13981  subrgugrp  14077  lspval  14227  ixpsnbasval  14303  lidlnegcl  14322  rspcl  14328  rspssid  14329  rspssp  14331  rspsn  14371  zrhmulg  14457  znzrhval  14484  mplsubgfilemm  14535  mplsubgfilemcl  14536  mplsubgfileminv  14537  mplnegfi  14542  ntrval  14657  clsval  14658  neival  14690  cnpval  14745  txmetcnp  15065  metcnpd  15067  limccl  15206  ellimc3apf  15207  cnplimclemr  15216  limccnp2cntop  15224  dvfvalap  15228  dvfre  15257  plycoeid3  15304  plyrecj  15310  lgsval4  15572  lgsmod  15578  2omap  16071  pw1map  16073  peano4nninf  16084