Theorem fveq1d 5650

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

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

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 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341

This theorem is referenced by:  fveq12d  5655  funssfv  5674  fv2prc  5687  csbfv2g  5689  fvco4  5727  fvmptd  5736  fvmpt2d  5742  mpteqb  5746  fvmptt  5747  fnmptfvd  5760  fmptco  5821  fvunsng  5856  fvsng  5858  fsnunfv  5863  f1ocnvfv1  5928  f1ocnvfv2  5929  fcof1  5934  fcofo  5935  ofvalg  6254  offval2  6260  ofrfval2  6261  caofinvl  6270  tfrlemi1  6541  rdg0g  6597  freceq1  6601  oav  6665  omv  6666  oeiv  6667  pw2f1odclem  7063  mapxpen  7077  xpmapenlem  7078  nninfisollemne  7373  nninfisol  7375  exmidomni  7384  nninfwlpoimlemginf  7418  cc3  7530  fseq1p1m1  10374  seqeq3  10760  seq3f1olemqsum  10821  seq3f1olemstep  10822  seq3f1olemp  10823  seqf1oglem2  10828  seqf1og  10829  seq3id  10833  seq3z  10836  exp3val  10849  bcval5  11071  bcn2  11072  seq3coll  11152  s1fv  11252  ccat1st1st  11267  ccat2s1fvwd  11273  swrdfv  11283  pfxfv  11314  swrdswrd  11335  shftcan1  11457  shftcan2  11458  shftvalg  11459  shftval4g  11460  climshft2  11929  sumeq2  11982  summodc  12007  zsumdc  12008  fsum3  12011  isumz  12013  fisumss  12016  fsum3cvg2  12018  isumsplit  12115  prodeq2w  12180  prodeq2  12181  prodmodc  12202  zproddc  12203  fprodseq  12207  prod1dc  12210  fprodssdc  12214  nninfctlemfo  12674  odzval  12877  1arithlem2  13000  fvsetsid  13179  setsslid  13196  setsslnid  13197  prdsex  13415  prdsval  13419  prdsplusgfval  13430  prdsmulrfval  13432  imasival  13452  imasbas  13453  imasplusg  13454  imasmulr  13455  igsumvalx  13535  gsumfzval  13537  gsumpropd  13538  gsumress  13541  gsumval2  13543  grpinvval  13689  grpsubfvalg  13691  grpsubpropdg  13750  grpsubpropd2  13751  pwsinvg  13758  mulgfvalg  13771  mulgpropdg  13814  submmulg  13816  subgmulg  13838  releqgg  13870  eqgex  13871  eqgfval  13872  gsumfzmptfidmadd  13989  unitinvcl  14201  unitinvinv  14202  unitlinv  14204  unitrinv  14205  unitnegcl  14208  dvrfvald  14211  dvrvald  14212  rdivmuldivd  14222  subrgugrp  14318  rrgsupp  14344  lspval  14469  ixpsnbasval  14545  lidlnegcl  14564  rspcl  14570  rspssid  14571  rspssp  14573  rspsn  14613  zrhmulg  14699  znzrhval  14726  mplsubgfilemm  14782  mplsubgfilemcl  14783  mplsubgfileminv  14784  mplnegfi  14789  ntrval  14904  clsval  14905  neival  14937  cnpval  14992  txmetcnp  15312  metcnpd  15314  limccl  15453  ellimc3apf  15454  cnplimclemr  15463  limccnp2cntop  15471  dvfvalap  15475  dvfre  15504  plycoeid3  15551  plyrecj  15557  lgsval4  15822  lgsmod  15828  uhgrspansubgrlem  16200  vtxdgfval  16212  vtxdgfifival  16215  vtxdgop  16216  vtxdeqd  16220  vtxdfifiun  16221  1loopgrvd0fi  16230  1hevtxdg0fi  16231  1hevtxdg1en  16232  1hegrvtxdg1fi  16233  wksfval  16246  wlkres  16303  eupth2fi  16403  2omap  16698  pw1map  16700  peano4nninf  16715  gsumgfsumlem  16795