Theorem fveq1d 5641

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

Syntax hints:   → wi 4   = wceq 1397  ‘cfv 5326

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334

This theorem is referenced by:  fveq12d  5646  funssfv  5665  fv2prc  5678  csbfv2g  5680  fvco4  5718  fvmptd  5727  fvmpt2d  5733  mpteqb  5737  fvmptt  5738  fnmptfvd  5751  fmptco  5813  fvunsng  5848  fvsng  5850  fsnunfv  5855  f1ocnvfv1  5918  f1ocnvfv2  5919  fcof1  5924  fcofo  5925  ofvalg  6245  offval2  6251  ofrfval2  6252  caofinvl  6261  tfrlemi1  6498  rdg0g  6554  freceq1  6558  oav  6622  omv  6623  oeiv  6624  pw2f1odclem  7020  mapxpen  7034  xpmapenlem  7035  nninfisollemne  7330  nninfisol  7332  exmidomni  7341  nninfwlpoimlemginf  7375  cc3  7487  fseq1p1m1  10329  seqeq3  10715  seq3f1olemqsum  10776  seq3f1olemstep  10777  seq3f1olemp  10778  seqf1oglem2  10783  seqf1og  10784  seq3id  10788  seq3z  10791  exp3val  10804  bcval5  11026  bcn2  11027  seq3coll  11107  s1fv  11207  ccat1st1st  11222  ccat2s1fvwd  11228  swrdfv  11238  pfxfv  11269  swrdswrd  11290  shftcan1  11412  shftcan2  11413  shftvalg  11414  shftval4g  11415  climshft2  11884  sumeq2  11937  summodc  11962  zsumdc  11963  fsum3  11966  isumz  11968  fisumss  11971  fsum3cvg2  11973  isumsplit  12070  prodeq2w  12135  prodeq2  12136  prodmodc  12157  zproddc  12158  fprodseq  12162  prod1dc  12165  fprodssdc  12169  nninfctlemfo  12629  odzval  12832  1arithlem2  12955  fvsetsid  13134  setsslid  13151  setsslnid  13152  prdsex  13370  prdsval  13374  prdsplusgfval  13385  prdsmulrfval  13387  imasival  13407  imasbas  13408  imasplusg  13409  imasmulr  13410  igsumvalx  13490  gsumfzval  13492  gsumpropd  13493  gsumress  13496  gsumval2  13498  grpinvval  13644  grpsubfvalg  13646  grpsubpropdg  13705  grpsubpropd2  13706  pwsinvg  13713  mulgfvalg  13726  mulgpropdg  13769  submmulg  13771  subgmulg  13793  releqgg  13825  eqgex  13826  eqgfval  13827  gsumfzmptfidmadd  13944  unitinvcl  14156  unitinvinv  14157  unitlinv  14159  unitrinv  14160  unitnegcl  14163  dvrfvald  14166  dvrvald  14167  rdivmuldivd  14177  subrgugrp  14273  lspval  14423  ixpsnbasval  14499  lidlnegcl  14518  rspcl  14524  rspssid  14525  rspssp  14527  rspsn  14567  zrhmulg  14653  znzrhval  14680  mplsubgfilemm  14731  mplsubgfilemcl  14732  mplsubgfileminv  14733  mplnegfi  14738  ntrval  14853  clsval  14854  neival  14886  cnpval  14941  txmetcnp  15261  metcnpd  15263  limccl  15402  ellimc3apf  15403  cnplimclemr  15412  limccnp2cntop  15420  dvfvalap  15424  dvfre  15453  plycoeid3  15500  plyrecj  15506  lgsval4  15768  lgsmod  15774  uhgrspansubgrlem  16146  vtxdgfval  16158  vtxdgfifival  16161  vtxdgop  16162  vtxdeqd  16166  vtxdfifiun  16167  1loopgrvd0fi  16176  1hevtxdg0fi  16177  1hevtxdg1en  16178  1hegrvtxdg1fi  16179  wksfval  16192  wlkres  16249  eupth2fi  16349  2omap  16645  pw1map  16647  peano4nninf  16659  gsumgfsumlem  16735