Theorem fveq1d 5517

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

Syntax hints:   → wi 4   = wceq 1353  ‘cfv 5216

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-uni 3810  df-br 4004  df-iota 5178  df-fv 5224

This theorem is referenced by:  fveq12d  5522  funssfv  5541  csbfv2g  5552  fvco4  5588  fvmptd  5597  fvmpt2d  5602  mpteqb  5606  fvmptt  5607  fnmptfvd  5620  fmptco  5682  fvunsng  5710  fvsng  5712  fsnunfv  5717  f1ocnvfv1  5777  f1ocnvfv2  5778  fcof1  5783  fcofo  5784  ofvalg  6091  offval2  6097  ofrfval2  6098  caofinvl  6104  tfrlemi1  6332  rdg0g  6388  freceq1  6392  oav  6454  omv  6455  oeiv  6456  mapxpen  6847  xpmapenlem  6848  nninfisollemne  7128  nninfisol  7130  exmidomni  7139  nninfwlpoimlemginf  7173  cc3  7266  fseq1p1m1  10093  seqeq3  10449  seq3f1olemqsum  10499  seq3f1olemstep  10500  seq3f1olemp  10501  seq3id  10507  seq3z  10510  exp3val  10521  bcval5  10742  bcn2  10743  seq3coll  10821  shftcan1  10842  shftcan2  10843  shftvalg  10844  shftval4g  10845  climshft2  11313  sumeq2  11366  summodc  11390  zsumdc  11391  fsum3  11394  isumz  11396  fisumss  11399  fsum3cvg2  11401  isumsplit  11498  prodeq2w  11563  prodeq2  11564  prodmodc  11585  zproddc  11586  fprodseq  11590  prod1dc  11593  fprodssdc  11597  odzval  12240  1arithlem2  12361  fvsetsid  12495  setsslid  12512  setsslnid  12513  prdsex  12717  imasival  12726  imasbas  12727  imasplusg  12728  imasmulr  12729  grpinvval  12915  grpsubfvalg  12917  grpsubpropdg  12973  grpsubpropd2  12974  mulgfvalg  12984  mulgpropdg  13023  subgmulg  13046  releqgg  13078  eqgfval  13079  unitinvcl  13290  unitinvinv  13291  unitlinv  13293  unitrinv  13294  unitnegcl  13297  dvrfvald  13300  dvrvald  13301  rdivmuldivd  13311  subrgugrp  13359  ntrval  13580  clsval  13581  neival  13613  cnpval  13668  txmetcnp  13988  metcnpd  13990  limccl  14098  ellimc3apf  14099  cnplimclemr  14108  limccnp2cntop  14116  dvfvalap  14120  dvfre  14144  lgsval4  14391  lgsmod  14397  peano4nninf  14725