Theorem fveq1d 5677

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

Syntax hints:   → wi 4   = wceq 1398  ‘cfv 5357

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365

This theorem is referenced by:  fveq12d  5682  funssfv  5701  fv2prc  5714  csbfv2g  5716  fvco4  5754  fvmptd  5763  fvmpt2d  5769  mpteqb  5773  fvmptt  5774  fnmptfvd  5787  fmptco  5848  fvunsng  5883  fvsng  5885  fsnunfv  5890  f1ocnvfv1  5956  f1ocnvfv2  5957  fcof1  5962  fcofo  5963  ofvalg  6285  offval2  6291  ofrfval2  6292  caofinvl  6301  tfrlemi1  6576  rdg0g  6632  freceq1  6636  oav  6700  omv  6701  oeiv  6702  pw2f1odclem  7100  mapxpen  7114  xpmapenlem  7115  2omap  7282  nninfisollemne  7435  nninfisol  7437  exmidomni  7446  nninfwlpoimlemginf  7480  cc3  7598  fseq1p1m1  10450  seqeq3  10838  seq3f1olemqsum  10899  seq3f1olemstep  10900  seq3f1olemp  10901  seqf1oglem2  10906  seqf1og  10907  seq3id  10911  seq3z  10914  exp3val  10927  bcval5  11150  bcn2  11151  seq3coll  11239  s1fv  11339  ccat1st1st  11354  ccat2s1fvwd  11360  swrdfv  11370  pfxfv  11401  swrdswrd  11422  shftcan1  11544  shftcan2  11545  shftvalg  11546  shftval4g  11547  climshft2  12016  sumeq2  12069  summodc  12094  zsumdc  12095  fsum3  12098  isumz  12100  fisumss  12103  fsum3cvg2  12105  isumsplit  12202  prodeq2w  12267  prodeq2  12268  prodmodc  12289  zproddc  12290  fprodseq  12294  prod1dc  12297  fprodssdc  12301  nninfctlemfo  12761  odzval  12964  1arithlem2  13087  ballotfileme  13180  ballotfilemi  13187  ballotfi  13226  fvsetsid  13330  setsslid  13347  setsslnid  13348  imasival  13570  imasbas  13571  imasplusg  13572  imasmulr  13573  igsumvalx  13652  gsumfzval  13654  gsumpropd  13655  gsumress  13658  gsumval2  13660  grpinvval  13798  grpsubfvalg  13800  grpsubpropdg  13859  grpsubpropd2  13860  mulgfvalg  13874  mulgpropdg  13917  submmulg  13919  subgmulg  13941  releqgg  13973  eqgex  13974  eqgfval  13975  gsumfzmptfidmadd  14092  gsumshift  14105  prdsex  14114  prdsval  14115  prdsplusgfval  14126  prdsmulrfval  14128  pwsinvg  14157  unitinvcl  14368  unitinvinv  14369  unitlinv  14371  unitrinv  14372  unitnegcl  14375  dvrfvald  14378  dvrvald  14379  rdivmuldivd  14389  subrgugrp  14486  rrgsupp  14512  opprdrng  14558  lspval  14664  ixpsnbasval  14740  lidlnegcl  14759  rspcl  14765  rspssid  14766  rspssp  14768  rspsn  14808  zrhmulg  14894  znzrhval  14921  mplsubgfilemm  14979  mplsubgfilemcl  14980  mplsubgfileminv  14981  mplnegfi  14986  ntrval  15101  clsval  15102  neival  15134  cnpval  15189  txmetcnp  15509  metcnpd  15511  limccl  15650  ellimc3apf  15651  cnplimclemr  15660  limccnp2cntop  15668  dvfvalap  15672  dvfre  15701  plycoeid3  15748  plyrecj  15754  lgsval4  16019  lgsmod  16025  uhgrspansubgrlem  16397  vtxdgfval  16409  vtxdgfifival  16412  vtxdgop  16413  vtxdeqd  16417  vtxdfifiun  16418  1loopgrvd0fi  16427  1hevtxdg0fi  16428  1hevtxdg1en  16429  1hegrvtxdg1fi  16430  wksfval  16443  wlkres  16500  eupth2fi  16600  pw1map  16895  peano4nninf  16910