Theorem fveq1d 5692

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

Syntax hints:   → wi 4   = wceq 1402  ‘cfv 5372

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-uni 3931  df-br 4126  df-iota 5332  df-fv 5380

This theorem is referenced by:  fveq12d  5697  funssfv  5716  fv2prc  5729  csbfv2g  5731  fvco4  5771  fvmptd  5780  fvmpt2d  5786  mpteqb  5790  fvmptt  5791  fnmptfvd  5804  fmptco  5865  fvunsng  5900  fvsng  5902  fsnunfv  5907  f1ocnvfv1  5973  f1ocnvfv2  5974  fcof1  5979  fcofo  5980  ofvalg  6302  offval2  6308  ofrfval2  6309  caofinvl  6318  tfrlemi1  6593  rdg0g  6649  freceq1  6653  oav  6717  omv  6718  oeiv  6719  pw2f1odclem  7124  mapxpen  7138  xpmapenlem  7139  2omap  7308  nninfisollemne  7461  nninfisol  7463  exmidomni  7472  nninfwlpoimlemginf  7506  cc3  7624  fseq1p1m1  10479  seqeq3  10867  seq3f1olemqsum  10928  seq3f1olemstep  10929  seq3f1olemp  10930  seqf1oglem2  10935  seqf1og  10936  seq3id  10940  seq3z  10943  exp3val  10956  bcval5  11179  bcn2  11180  hashf1lem1  11263  seq3coll  11272  s1fv  11372  ccat1st1st  11387  ccat2s1fvwd  11393  swrdfv  11403  pfxfv  11434  swrdswrd  11455  shftcan1  11577  shftcan2  11578  shftvalg  11579  shftval4g  11580  climshft2  12050  sumeq2  12103  summodc  12128  zsumdc  12129  fsum3  12132  isumz  12134  fisumss  12137  fsum3cvg2  12139  isumsplit  12236  prodeq2w  12301  prodeq2  12302  prodmodc  12323  zproddc  12324  fprodseq  12328  prod1dc  12331  fprodssdc  12335  nninfctlemfo  12795  odzval  12998  1arithlem2  13121  ballotfileme  13214  ballotfilemi  13221  ballotfi  13260  fvsetsid  13364  setsslid  13381  setsslnid  13382  imasival  13604  imasbas  13605  imasplusg  13606  imasmulr  13607  gzsumvalx  13686  gzsumfzval  13688  gzsumress  13689  gzsumval2  13691  grpinvval  13825  grpsubfvalg  13827  grpsubpropdg  13886  grpsubpropd2  13887  mulgfvalg  13901  mulgpropdg  13944  submmulg  13946  subgmulg  13968  releqgg  14000  eqgex  14001  eqgfval  14002  gzsumshift  14126  prdsex  14149  prdsval  14150  prdsplusgfval  14161  prdsmulrfval  14163  pwsinvg  14192  unitinvcl  14403  unitinvinv  14404  unitlinv  14406  unitrinv  14407  unitnegcl  14410  dvrfvald  14413  dvrvald  14414  rdivmuldivd  14424  subrgugrp  14521  rrgsupp  14547  opprdrng  14593  lspval  14699  ixpsnbasval  14775  lidlnegcl  14794  rspcl  14800  rspssid  14801  rspssp  14803  rspsn  14843  zrhmulg  14927  znzrhval  14954  mplsubgfilemm  15012  mplsubgfilemcl  15013  mplsubgfileminv  15014  mplnegfi  15019  ntrval  15134  clsval  15135  neival  15167  cnpval  15222  txmetcnp  15542  metcnpd  15544  limccl  15683  ellimc3apf  15684  cnplimclemr  15693  limccnp2cntop  15701  dvfvalap  15705  dvfre  15734  plycoeid3  15781  plyrecj  15787  lgsval4  16053  lgsmod  16059  uhgrspansubgrlem  16431  vtxdgfval  16443  vtxdgfifival  16446  vtxdgop  16447  vtxdeqd  16451  vtxdfifiun  16452  1loopgrvd0fi  16461  1hevtxdg0fi  16462  1hevtxdg1en  16463  1hegrvtxdg1fi  16464  wksfval  16477  wlkres  16534  eupth2fi  16634  pw1map  16939  peano4nninf  16954